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