|
\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
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
