Quelle  TimeStamp.vdmpp   Sprache: VDM

\begin{vdm_al}
class TimeStamp

values

public stepLength : nat = 1;

instance variables

currentTime  : nat   := 0;
wakeUpMap    : map nat to [nat] := {|->};
barrierCount : nat := 0;
registeredThreads : set of BaseThread := {};
isInitialising : bool := true;
-- singleton instance of class
private static timeStamp : TimeStamp := new TimeStamp();

operations

-- private constructor (singleton pattern)
private TimeStamp : () ==> TimeStamp
TimeStamp() ==
 skip;

-- public operation to get the singleton instance
pure public static GetInstance: () ==> TimeStamp
GetInstance() ==
  return timeStamp;

public RegisterThread : BaseThread ==> ()
RegisterThread(t) ==
 (barrierCount := barrierCount + 1;
  registeredThreads := registeredThreads union {t};  
 );
 
public UnRegisterThread : BaseThread ==> ()
UnRegisterThread(t) ==
 (barrierCount := barrierCount - 1;
  registeredThreads := registeredThreads \ {t};
 );
 
public IsInitialising: () ==> bool
IsInitialising() ==
  return isInitialising;
 
public DoneInitialising: () ==> ()
DoneInitialising() ==
 (if isInitialising
  then (isInitialising := false;
        for all t in set registeredThreads 
        do
          start(t);
       );
 );

public WaitRelative : nat ==> ()
WaitRelative(val) ==
 (WaitAbsolute(currentTime + val);  
 );
 
public WaitAbsolute : nat ==> ()
WaitAbsolute(val) == (
  AddToWakeUpMap(threadid, val);
  -- Last to enter the barrier notifies the rest.
  BarrierReached();
  -- Wait till time is up
  Awake();
);

BarrierReached : () ==> ()
BarrierReached() == 
(
 while (card dom wakeUpMap = barrierCount) do
   (
    currentTime := currentTime + stepLength;
    let threadSet : set of nat = {th | th in set dom wakeUpMap 
             & wakeUpMap(th) <> nil and wakeUpMap(th) <= currentTime }
  in
   for all t in set threadSet 
   do
    wakeUpMap := {t} <-: wakeUpMap;
 );
)
post forall x in set rng wakeUpMap & x = nil or x >= currentTime;

AddToWakeUpMap : nat * [nat] ==> ()
AddToWakeUpMap(tId, val) ==
   wakeUpMap := wakeUpMap ++ { tId |-> val };

public NotifyThread : nat ==> ()
NotifyThread(tId) ==
 wakeUpMap := {tId} <-: wakeUpMap;

pure public GetTime : () ==> nat
GetTime() ==
  return currentTime;

Awake: () ==> ()
Awake() == skip;

public ThreadDone : () ==> ()
ThreadDone() == 
 AddToWakeUpMap(threadid, nil);

sync
  per Awake => threadid not in set dom wakeUpMap;

  mutex (IsInitialising);
  mutex (DoneInitialising);
  
  mutex (AddToWakeUpMap);
  mutex (NotifyThread);
  mutex (BarrierReached);
  
  mutex (AddToWakeUpMap, NotifyThread);
  mutex (AddToWakeUpMap, BarrierReached);
  mutex (NotifyThread, BarrierReached);
  
  mutex (AddToWakeUpMap, NotifyThread, BarrierReached);

end TimeStamp