MODULE Monitor;

  IMPORT WinApi;
 
  TYPE
    Handle* = POINTER TO LIMITED RECORD
      count: INTEGER;
      enter, pulse: WinApi.HANDLE
    END;

  PROCEDURE New* (): Handle;
    VAR h: Handle;
  BEGIN NEW(h);
    h.enter := WinApi.CreateEvent(NIL, WinApi.FALSE, WinApi.TRUE, NIL);
    h.pulse := WinApi.CreateEvent(NIL, WinApi.TRUE, WinApi.FALSE, NIL);
    RETURN h
  END New;

  PROCEDURE Enter* (h: Handle);
    VAR res: INTEGER;
  BEGIN
    IF WinApi.InterlockedIncrement(h.count) # 1 THEN
      res := WinApi.WaitForSingleObject(h.enter, WinApi.INFINITE)
    END
  END Enter;

  PROCEDURE Exit* (h: Handle);
    VAR ok: WinApi.BOOL;
  BEGIN
    IF WinApi.InterlockedDecrement(h.count) # 0 THEN
      ok := WinApi.SetEvent(h.enter)
    END
  END Exit;

  PROCEDURE Wait* (h: Handle);
    VAR res: INTEGER;
  BEGIN   
    res := WinApi.SignalObjectAndWait(h.enter, h.pulse, WinApi.INFINITE, WinApi.FALSE);
    res := WinApi.InterlockedDecrement(h.count);
    Enter(h)
  END Wait;

  PROCEDURE Pulse* (h: Handle);
    VAR ok: WinApi.BOOL;
  BEGIN ok := WinApi.PulseEvent(h.pulse)
  END Pulse;

  PROCEDURE (h: Handle) FINALIZE-;
    VAR ok: WinApi.BOOL;
  BEGIN
    ok := WinApi.CloseHandle(h.pulse);
    ok := WinApi.CloseHandle(h.enter)
  END FINALIZE;

END Monitor.

  IMPORT Monitor;

  TYPE
    Element* = INTEGER;

    Queue* = POINTER TO LIMITED RECORD
      synchRoot: Monitor.Handle;
      buffer: ARRAY 3 OF Element;
      begin, end, count, enqueued, dequeued: INTEGER;
    END;

  PROCEDURE NewQueue* (): Queue;
    VAR q: Queue;
  BEGIN NEW(q);
    q.synchRoot := Monitor.New();
    RETURN q
  END NewQueue;

  PROCEDURE (q: Queue) Enqueue* (e: Element), NEW;
  BEGIN
    Monitor.Enter(q.synchRoot);
    WHILE q.count >= LEN(q.buffer) DO Monitor.Wait(q.synchRoot) END;
    INC(q.count);
    INC(q.enqueued);
    q.buffer[q.end] := e;
    q.end := (q.end + 1) MOD LEN(q.buffer);
    Monitor.Pulse(q.synchRoot);
    Monitor.Exit(q.synchRoot)
  END Enqueue;

  PROCEDURE (q: Queue) Dequeue* (OUT e: Element), NEW;
  BEGIN
    Monitor.Enter(q.synchRoot);
    WHILE q.count < 1 DO Monitor.Wait(q.synchRoot) END;
    DEC(q.count);
    INC(q.dequeued);
    e := q.buffer[q.begin];
    q.begin := (q.begin + 1) MOD LEN(q.buffer);
    Monitor.Pulse(q.synchRoot);
    Monitor.Exit(q.synchRoot)
  END Dequeue;

FOR i := 1 TO N DO
  Monitor.Enter(h);
  Monitor.Exit(h)
END;

FOR i := 1 TO N DO
  INC(s); INC(s); INC(s); INC(s); INC(s);
  INC(s); INC(s); INC(s); INC(s); INC(s)
END;

DEFINITION Hoare;

  TYPE
    Monitor = POINTER TO LIMITED RECORD
      (m: Monitor) Enter, NEW;
      (m: Monitor) Exit, NEW;
      (m: Monitor) FINALIZE-
    END;

    Condition = POINTER TO LIMITED RECORD
      (c: Condition) Signal, NEW;
      (c: Condition) Wait, NEW;
      (c: Condition) FINALIZE-
    END;

  PROCEDURE NewMonitor (): Monitor;
  PROCEDURE NewCondition (m: Monitor): Condition;

END Hoare.

  IMPORT Hoare;

  TYPE
    Element* = INTEGER;

    Queue* = POINTER TO LIMITED RECORD
      monitor: Hoare.Monitor;
      nonEmpty, nonFull: Hoare.Condition;
      buffer: ARRAY 3 OF Element;
      begin, end, count, enqueued, dequeued: INTEGER;
    END;

  PROCEDURE NewQueue* (): Queue;
    VAR q: Queue;
  BEGIN NEW(q);
    q.monitor := Hoare.NewMonitor();
    q.nonEmpty := Hoare.NewCondition(q.monitor);
    q.nonFull := Hoare.NewCondition(q.monitor);
    RETURN q
  END NewQueue;

  PROCEDURE (q: Queue) Enqueue* (e: Element), NEW;
  BEGIN
    q.monitor.Enter;
    WHILE q.count >= LEN(q.buffer) DO q.nonFull.Wait END;
    INC(q.count);
    INC(q.enqueued);
    q.buffer[q.end] := e;
    q.end := (q.end + 1) MOD LEN(q.buffer);
    q.nonEmpty.Signal;
    q.monitor.Exit
  END Enqueue;

  PROCEDURE (q: Queue) Dequeue* (OUT e: Element), NEW;
  BEGIN
    q.monitor.Enter;
    WHILE q.count < 1 DO q.nonEmpty.Wait END;
    DEC(q.count);
    INC(q.dequeued);
    e := q.buffer[q.begin];
    q.begin := (q.begin + 1) MOD LEN(q.buffer);
    q.nonFull.Signal;
    q.monitor.Exit
  END Dequeue;

MODULE Hoare;

  IMPORT WinApi;
 
  TYPE
    Monitor* = POINTER TO LIMITED RECORD
      n: INTEGER;
      h: WinApi.HANDLE
    END;

    Condition* = POINTER TO LIMITED RECORD
      m: Monitor;
      h: WinApi.HANDLE
    END;

  PROCEDURE NewMonitor* (): Monitor;
    VAR m: Monitor;
  BEGIN NEW(m);
    m.h := WinApi.CreateEvent(NIL, WinApi.FALSE, WinApi.TRUE, NIL);
    RETURN m
  END NewMonitor;

  PROCEDURE NewCondition* (m: Monitor): Condition;
    VAR c: Condition;
  BEGIN ASSERT(m # NIL, 20);
    NEW(c);
    c.m := m;
    c.h := WinApi.CreateEvent(NIL, WinApi.TRUE, WinApi.FALSE, NIL);
    RETURN c
  END NewCondition;

  PROCEDURE (m: Monitor) Enter*, NEW;
    VAR res: INTEGER;
  BEGIN
    IF WinApi.InterlockedIncrement(m.n) # 1 THEN
      res := WinApi.WaitForSingleObject(m.h, WinApi.INFINITE)
    END
  END Enter;

  PROCEDURE (m: Monitor) Exit*, NEW;
    VAR ok: WinApi.BOOL;
  BEGIN
    IF WinApi.InterlockedDecrement(m.n) # 0 THEN
      ok := WinApi.SetEvent(m.h)
    END
  END Exit;

  PROCEDURE (c: Condition) Wait*, NEW;
    VAR res: INTEGER;
  BEGIN   
    res := WinApi.SignalObjectAndWait(c.m.h, c.h, WinApi.INFINITE, WinApi.FALSE);
    res := WinApi.InterlockedDecrement(c.m.n);
    c.m.Enter
  END Wait;

  PROCEDURE (c: Condition) Signal*, NEW;
    VAR ok: WinApi.BOOL;
  BEGIN ok := WinApi.PulseEvent(c.h)
  END Signal;

  PROCEDURE (m: Monitor) FINALIZE-;
    VAR ok: WinApi.BOOL;
  BEGIN
    (* ok := WinApi.CloseHandle(h.pulse); *)
    ok := WinApi.CloseHandle(m.h)
  END FINALIZE;

  PROCEDURE (c: Condition) FINALIZE-;
    VAR ok: WinApi.BOOL;
  BEGIN
    ok := WinApi.CloseHandle(c.h)
  END FINALIZE;

END Hoare.

Semaphore = POINTER TO ABSTRACT RECORD
  (sem: Semaphore) POST (n: INTEGER), NEW, ABSTRACT;
  (sem: Semaphore) WAIT, NEW, ABSTRACT
END;

MODULE Hoare;

   IMPORT WinApi;

   TYPE
      Monitor* = POINTER TO LIMITED RECORD
         cs: WinApi.CRITICAL_SECTION
      END;

      Condition* = POINTER TO LIMITED RECORD
         monitor: Monitor;
         n: INTEGER;
         list: ARRAY 256 OF WinApi.HANDLE
      END;

   PROCEDURE NewMonitor* (): Monitor;
      VAR m: Monitor;
   BEGIN NEW(m);
      WinApi.InitializeCriticalSection(m.cs);
      RETURN m
   END NewMonitor;

   PROCEDURE NewCondition* (m: Monitor): Condition;
      VAR c: Condition;
   BEGIN ASSERT(m # NIL, 20);
      NEW(c); c.monitor := m;
      RETURN c
   END NewCondition;

   PROCEDURE (m: Monitor) Enter*, NEW;
   BEGIN WinApi.EnterCriticalSection(m.cs)
   END Enter;

   PROCEDURE (m: Monitor) Exit*, NEW;
   BEGIN WinApi.LeaveCriticalSection(m.cs)
   END Exit;

   PROCEDURE APCEmpty (param: INTEGER);
   END APCEmpty;

   PROCEDURE (c: Condition) Signal*, NEW;
      VAR i, res: INTEGER;
   BEGIN
      IF c.n > 0 THEN
         FOR i := 0 TO c.n - 1 DO
            res := WinApi.QueueUserAPC(APCEmpty, c.list[i], 0);
            res := WinApi.CloseHandle(c.list[i])
         END;
         c.n := 0
      END
   END Signal;

   PROCEDURE (c: Condition) Wait*, NEW;
      CONST access = {0, 1, 3, 4, 16..19}; opt = {};
      VAR res: INTEGER; p: WinApi.HANDLE;
   BEGIN
      IF c.n < LEN(c.list) THEN
         p := WinApi.GetCurrentProcess();
         res := WinApi.DuplicateHandle(p, WinApi.GetCurrentThread(), p, c.list[c.n], access, 0, opt);
         INC(c.n);
         WinApi.LeaveCriticalSection(c.monitor.cs);
         res := WinApi.SleepEx(WinApi.INFINITE, WinApi.TRUE);
         WinApi.EnterCriticalSection(c.monitor.cs)
      ELSE
         WinApi.LeaveCriticalSection(c.monitor.cs);
         WinApi.Sleep(20);
         WinApi.EnterCriticalSection(c.monitor.cs)
      END
   END Wait;

   PROCEDURE (m: Monitor) FINALIZE-;
   BEGIN WinApi.DeleteCriticalSection(m.cs)
   END FINALIZE;

END Hoare.