On Friday 28 Nov 2008 11:06 am, David Matthews wrote:
Phil,
Philip Clayton wrote:
My understanding of loading a state is that new objects are created whether or not the same object is already loaded. That seems the right thing to do, as you say. When loading a child state however, I would expect only objects in the child state to be created and any objects not in the child to remain as they are. This does not appear to fit with our observations in relation to threads though. Loading a child state appears to prevent a running thread from picking up the latest mutable data, even though all objects used in the running thread are not in the child state. I can't recreate the issue without threads. I've updated the previous example to show this.
I've had a look through your example and I'm not certain exactly what's going on but I think the answer is that loading a child state always (re)loads the parents, at least as the code is currently implemented. This causes a new version of your ref "c" to be created and breaks the link between the ref that the thread is using and the ref that is found by looking up "c".
This may be obvious, but you don't need threads to exhibit this issue. E.g.,
val c1 = ref 1;
PolyML.SaveState.saveState "test1.polydb"; (* save state with c1 = ref 1 *)
val c2 = c1; (c1 := 2; c2); (* val it = ref 2 *)
PolyML.SaveState.saveChild ("test2.polydb", 1); (* save state with c2 = c1 & c1 = ref 1 *)
val c3 = c1; (c1 := 3; c3); (* val it = ref 2 *)
(* load the child test2.polydb *) val c4 = (PolyML.SaveState.loadState "test2.polydb"; c3);
c1; (* val it = ref 2 *) c4; (* val it = ref 3 *) c3; (* Error-Value or constructor (c3) has not been declared *)
(c4 := 9; (c1, c4));(* val it = (ref 2, ref 9) *) (c1 := 5; (c1, c4));(* val it = (ref 5, ref 9) *)
I guess it would be possible to change this so that saved states that were already loaded were not reloaded. I can't think of any reasons why this wouldn't work. It would require changes to the code. However, I wonder if it's what users would always want. Aren't there cases where a user might want loadState on a child to restore the whole state?
I would expect it to restore only that part of the state that is referred to by the child and that does not exist, if that makes sense. I would not have expected it to undeclare c3 above and would have expected it to leave c1, c2, c3 and c4 all referencing the same cell.
What would be very useful would be if you could save immediate children of some state (say each containing some data and some code to operate on that data) and load them in independently with any pointers into the common ancestry being resolved in the obvious way.
In ProofPower, for example, we currently have to save and reload the entire state of the theory hierarchy. It would be nice if theories and associated proof procedures could be saved separately and only loaded when needed. HOL IV has some kind of home-rolled way of achieving something that looks like this under Moscow ML (which effectively doesn't allow data to be saved at all, but does allow modules of code to be saved separately).
Regards,
Rob.