Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/VDM/VDMPP/PacemakerConcPP/ (Wiener Entwicklungsmethode ^©) Datei vom 13.4.2020 mit Größe 2 kB

Quelle TimeStamp.vdmpp Sprache: VDM

\begin{vdm_al}
class TimeStamp

\end{vdm_al}
Modified by Johanne U. Jensen to act as a thread barrier.

Class used for concurrent VDM++ models. All threads should call the following operations:
- WaitRelative(t): makes the thread periodic with t = the period
- NotifyAll(): notified all threads sleeping in the wakeUpMap
- Awake(): puts the thread to sleep - will wakeup when t time units has passed

TimeStamp(nat1 barrierCount);

WaitRelative // blocks
WaitAbsolute // blocks

NotifyThread // Non blocking
GetTime // Non blocking

ThreadDone // Non Blocking

\begin{vdm_al}

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;

operations

public TimeStamp : nat ==> TimeStamp
TimeStamp(count) ==
barrierCount := count;

public RegisterThread : BaseThread ==> ()
RegisterThread(t) ==
(barrierCount := barrierCount + 1;
  registeredThreads := registeredThreads union {t};
);

public UnRegisterThread : () ==> ()
UnRegisterThread() ==
(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;

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);
  -- Is this really needed?
  mutex(AddToWakeUpMap);
  mutex(NotifyThread);
  mutex(BarrierReached);

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

  mutex(AddToWakeUpMap, NotifyThread, BarrierReached);

end TimeStamp

quality84%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.