-------------------------------------------------------------------------------

--* @author: P.H.Welch.
--* @title: Manager Oracle for Multiway Synchronisation (occam-pi).
--* @version: 1.0.
--* @date: 10/11/2005.
--* @acknowledgement: the idea for doing this was suggested by Ian Marshall.
--* @comment:
--*    Simple optimisation over version 0.0.  The search stops at the first
--*    completed multiway sync.  Not convinced this is worthwhile though?

-------------------------------------------------------------------------------

-- To compile this:
--
--  kroc -c mm-sync-oracle-1-0.occ

-------------------------------------------------------------------------------

--* A set of indices for multiway syncs on offer.
DATA TYPE OFFER IS MOBILE []INT:

--* The set of indices for processes enrolled on a multiway sync.
DATA TYPE ENROLLED IS MOBILE []INT:

--* NOTE: for the above types, `set' implies there are no repeated numbers
--*       in the array and their ordering has no significance.

--* NOTE: for this application, the above types contain only numbers >= 0.  

-------------------------------------------------------------------------------

--* Request channel protocol.
PROTOCOL ALT.SYNC.START IS
  INT;                      -- index of the ALTing process
  OFFER:                    -- the offer

--* Reply channel protocol.
PROTOCOL ALT.SYNC.FINISH IS
  INT;                      -- index of the chosen multiway sync
  OFFER:                    -- return the offer

-------------------------------------------------------------------------------

--* This process manages ALTing multiway synchronisation between (SIZE out)
--* application processes competing for (SIZE enrolled) events.
--*
--* @param enrolled: the indices of processes enrolled on each managed event.
--*
--* @param in?: the server channel to this multiway sync manager.
--*
--* @param out!: reply channels to each application process.
--*
--* CONTRACT: an offer from client (ALTing) process `i' must take the form:
--*
--*     in ? i; offer.i
--*
--*   (from the point of view of this process), where `offer.i' contains
--*   a subset of the events on which process `i' is enrolled.  Following
--*   such an offer, the client (ALTing) process must commit to accept:
--*
--*     out[i] ! chosen; offer.i
--*
--*   where `chosen' is an element of `offer.i' and indicates the multiway
--*   sync event chosen by this oracle.  Such a reply will not be made until
--*   a complete set of offers for the `chosen' event have been received.
--*   Of course, all the offering processes will receive the same `chosen'
--*   reply.
--*
--* NOTE: each `offer.i' is returned because this process has no further use
--* for it and the client probably does.
--*
PROC mm.sync.oracle (MOBILE []ENROLLED enrolled,
                     CHAN ALT.SYNC.START in?,
                     []CHAN ALT.SYNC.FINISH out!)

  --* counts of number of offers still needed for each multiway sync
  MOBILE []INT count:

  --* offers made by each application process
  MOBILE []OFFER offer:

  SEQ
    
    count := MOBILE [SIZE enrolled]INT
    SEQ j = 0 FOR SIZE count
      count[j] := SIZE enrolled[j]
    
    offer := MOBILE [SIZE out]OFFER

    WHILE TRUE

      --* INVARIANT: [ j = 0 FOR SIZE enrolled |
      --*              count[j] is the number of offers needed to complete
      --*              multiway sync `j' ]

      --* INVARIANT: [ i = 0 FOR SIZE offer |
      --*              (DEFINED offer[i]) <==>
      --*              (process `i' has made offer[i]) ]

      --* INVARIANT: [ j = 0 FOR SIZE enrolled |
      --*              (count[j] > 0) <==> (SIZE enrolled[j] > 0) ]

      -- The point of the last invariant is that, in this state, all multiway
      -- syncs (that have *some* customers enrolled) need at least one more
      -- offer before they can complete.

      INT app:

      OFFER this.offer:

      INITIAL INT j IS 0:           -- for indexing through offers

      INITIAL INT chosen IS -1:     -- initially, not chosen

      SEQ

        in ? app; this.offer
        --* DEDUCE: process `app' is enrolled on each sync in `this.offer'

        WHILE (chosen < 0) AND (j < (SIZE this.offer))
          SEQ
            VAL INT this.offer.j IS this.offer[j]:
            INT count.offer.j IS count[this.offer.j]:
            --* DEDUCE: count.offer.j > 0
            SEQ
              count.offer.j := count.offer.j - 1
              IF
                count.offer.j = 0
                  chosen := this.offer.j       --* DEDUCE: chosen >= 0
                TRUE
                  SKIP
            j := j + 1

        IF
          chosen >= 0
            SEQ

              -- restore counts decremented by this.offer (and reply)
              SEQ k = 0 FOR j
                INT count.offer.k IS count[this.offer[k]]:
                count.offer.k := count.offer.k + 1
              out[app] ! chosen; this.offer

              -- restore counts decremented by other offers (and reply)
              ENROLLED release IS enrolled[chosen]:
              SEQ i = 0 FOR SIZE release
                VAL INT release.i IS release[i]:
                IF
                  release.i <> app
                    OFFER next.offer IS offer[release.i]:
                    SEQ
                      --* ASSERT: DEFINED next.offer
                      SEQ j = 0 FOR SIZE next.offer
                        INT count.offer.j IS count[next.offer[j]]:
                        count.offer.j := count.offer.j + 1
                      out[release.i] ! chosen; next.offer
                      --* DEDUCE: ~(DEFINED next.offer)
                  TRUE
                    SKIP

          TRUE
            offer[app] := this.offer

: