From: Don Syme <dsyme@microsoft.com>
To: "'Xavier Leroy'" <Xavier.Leroy@inria.fr>, caml-list@inria.fr
Subject: RE: Break under Windows NT
Date: Tue, 16 Mar 1999 06:16:02 -0800
Hi Xavier,
Here are some more details:
I have an interactive theorem prover, whose interface is written using
OcamlTK, and which incorporates, for example, an editor and various feedback
windows, much like a traditional graphical IDE. The user sets the automated
prover running on various subgoals, one at a time, and feedback is generated
while the subgoal is being checked.
Firstly, users have to be able to interrupt the proof checking - until now
I've allowed them to hit Ctrl-C at the command line, thus generating a Break
exception in the application, which gets caught at the place where the
computation began. Under NT this causes the program to exit...
Beyond the Ctrl-C problem, I would ideally like to add proper
multi-threading. I've made some progress since yesterday toward doing this.
I've run several examples with threads+OcamlTK. The Tk stuff is being done
by one thread, and OCaml computations by other threads. This appears to
work fine. I've also got several crashes in situations where I've been
accessing OCamlTK from more than one thread, as you'd expect.
Because OCamlTK is not multithreaded, only the main thread (the one that
called Tk.mainLoop()) can do anything that involves the interface. In my
situation, this means that feedback generated from other threads must be
queued and periodically flushed/displayed by the main thread. I'm trying
this solution at the moment. Since X is not fully multithreaded (as far as
I know), I would imagine this would be a problem for any similar system
under X. The graphics code of Windows NT is, at least in principle,
multithreaded, so individual threads could then write to the interface.
I'll be looking at this sort of solution in a few months time.
BTW, perhaps OCamlTK could be delivered with a threaded version, which
provided some sort of mutex on access to TK functionality.
Also, I note the OCamlTK lib doesn't come with optimized compiled libraries,
e.g. tk41.cmxa. Is there any reason for this? Would it be a waste of time
to try to compile them optimized?
Finally, there seems to be a surprising performance hit when running
multiple threads under the bytecode interpreter with OCamlTK running. I'll
give more details if I manage to pin this down further - it might just be
that the interface is less responsive. This is also why I'm interested in
trying optimized OCaml with threads.
Cheers & many thanks,
Don
-----Original Message-----
From: Xavier Leroy [mailto:Xavier.Leroy@inria.fr]
Sent: 16 March 1999 13:51
To: Don Syme; caml-list@inria.fr
Subject: Re: Break under Windows NT
> Is it true that under the Windows NT version of OCaml there's no easy way
of
> sending the equivalent of a SIGINT to a OCaml process and have OCaml raise
> an exception?
As far as I know, Win32 has no equivalent to Unix signals (i.e. the
ability for a process to interrupt asynchronously another process).
For "console" applications, the C library implements some notion of
signals (for ANSI C compatibility), but SIGINT is only generated when
the user types ctrl-C or ctrl-break at the keyboard, or when the
program sends SIGINT to itself; it cannot be generated from another
process.
A classic alternative to signals is to use multiple threads: one
thread synchronously waits for some external notification, then fakes
a pending signal condition in the other thread that is running the
Caml code. However, Caml threads do not have (yet) the ability to
raise exceptions in other threads, so one has to implement this
solution in C. If you tell me in more details what you're trying to
achieve, maybe I could send you some sample code.
> Or have I missed something? I need to be able to
> asynchronously break long running computations under NT. BTW I'm also
using
> OCamlTK.
OCamlTk programs are not console-only applications, and thus have an
event loop that runs periodically. This adds more opportunities for
implementing inter-process notification, via periodic polling or
by posting special events on the application's message queue; however,
I haven't looked into this in details.
- Xavier Leroy
This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:21 MET