#INCLUDE "mm-sync-oracle-types.occ" #USE "course.lib" --* 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!, SHARED CHAN BYTE screen!) --* 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 INITIAL BOOL running IS TRUE: WHILE running --* 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: -- OFFER tmp: INITIAL INT chosen IS -1: -- initially, not chosen SEQ in ? app; this.offer IF app = terminate.oracle running := FALSE TRUE --* DEDUCE: process `app' is enrolled on each sync indexed in the offer SEQ SEQ j = 0 FOR SIZE this.offer VAL INT this.offer.j IS this.offer[j]: INT count.offer.j IS count[this.offer.j]: SEQ count.offer.j := count.offer.j - 1 IF (count.offer.j = 0) AND (chosen < 0) -- choose the first only chosen := this.offer.j --* DEDUCE: chosen >= 0 TRUE SKIP offer[app] := this.offer -- mobile assignment IF chosen >= 0 SEQ ENROLLED release IS enrolled[chosen]: SEQ i = 0 FOR SIZE release VAL INT release.i IS release[i]: 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 :