Philip Clayton wrote:
Does anyone know what should happen to threads (created with
Thread.Thread.fork) when PolyML.SaveState.loadState is performed? It
appears that they are no longer reported as active but, despite this,
carry on running. Is it up to the user to kill these before doing a
loadState?
Phil,
Threads continue running after loadState. However there is an issue
with thread identifiers and I think this is what is causing the confusion.
Saved states are primarily intended to allow the state to be restored in
a different session. Certain values, such as thread identifiers and
stream identifiers, only have meaning within a particular session and
aren't persistent. When they are saved and loaded, even within the same
session, the link with the original object is broken. It is possible to
"carry over" such a value within a session by passing it on the stack.
Consider:
val y = Thread.Mutex.mutex();
Thread.Mutex.lock y;
val v = Thread.Thread.fork(fn () => Thread.Mutex.lock y, []);
(* v now refers to a blocked but running thread. *)
PolyML.SaveState.saveState "save";
val w = (PolyML.SaveState.loadState "save"; v);
After reloading Poly/ML reports:
> Thread.Thread.isActive v;
val it = false : bool
> Thread.Thread.isActive w;
val it = true : bool
There is a similar situation with streams. The reason it works this way
is that there is no guarantee that the saved state loaded by loadState
actually has been loaded in the same session it was saved in. To solve
this would require (expensive) globally unique identifiers.
David
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
