overturetool
Sync guards don't notice field changes
The following bug was originally reported on Sourceforge by nick_battle, 2012-07-11 12:37:52.641000:
This is related to bug #147. If a sync guard uses the value of a field of an object, like "per op => obj.val", then it will (after the fix to #147) notice changes to the val field and trigger the guard, but if the obj member changes to a different object, changes to the val field thereafter will no longer be tracked.
The problem is that VDMJ determines the set of UpdatableValues that its sync clauses should listen to when an object instance is created. So if the expressions used in sync guards refer to different variables as the object evolves (eg. when "obj" changes above), then these will not be monitored correctly and the specification may deadlock.
The following illustrates the issue:
class Trigger
instance variables
public value:nat := 0
operations
public signal: () ==> ()
signal() == value := 1;
public reset: () ==> ()
reset() == value := 0;
sync
per signal => value = 0;
per reset => value = 1
end Trigger
class A
instance variables
trigger:Trigger := new Trigger()
operations
public run: () ==> ()
run() == while true do call();
public change: () ==> ()
change() == trigger := new Trigger();
public get: () ==> Trigger
get() == return trigger;
private call: () ==> ()
call() ==
(
IO`printf("Called %s\n", [trigger.value]);
trigger.reset()
)
sync
per call => trigger.value > 0;
thread
run()
end A
class Test
operations
public run: () ==> ()
run() ==
(
dcl a:A := new A();
let t:Trigger = a.get() in
(
start(a);
t.signal();
t.signal();
t.signal();
);
a.change();
let t:Trigger = a.get() in
(
t.signal();
t.signal();
t.signal();
);
)
end Test
Each time the t.signal() is called, the trigger allows the main thread to execute "call". But after the "change" method is called, subsequent changes to the new trigger value do not cause the sync guards in A to re-evaluate. This is because the guards are listening on the original trigger object's value. So the spec DEADLOCKs because t.signal blocks waiting for a.call to clear it (which will never happen, as call is blocked on the old trigger).
