--** Santa Claus: static network (no mobile channels or processes); -- asymmetric (reindeer use barrier, elves use partial barrier); -- waiting room reports. -- -- This is the solution discussed in Section 6 (and Appendix E) of the article: -- -- "Santa Claus: Formal analysis of a process-oriented solution" -- Welch, P. H. and Pedersen, J. B. -- ACM Trans. Program. Lang. Syst. 32, 4, Article 14 (April 2010), 37 pages. -- DOI =10.1145/1734206.1734211 http:/doi.acm.org/10.1145/1734206.1734211 #INCLUDE "protocol.occ" #INCLUDE "partial-barriers.occ" #INCLUDE "random-stuff.occ" #INCLUDE "display.occ" VAL INT N.REINDEER IS 9: VAL INT G.REINDEER IS N.REINDEER: VAL INT N.ELVES IS 10: VAL INT G.ELVES IS 3: VAL INT HOLIDAY.TIME IS 100000: -- microseconds VAL INT WORKING.TIME IS 200000: -- microseconds VAL INT DELIVERY.TIME IS 100000: -- microseconds VAL INT CONSULTATION.TIME IS 200000: -- microseconds PROC waiting.room (VAL INT n, CHAN BOOL a?, a.ack?, b?, ping!) WHILE TRUE SEQ SEQ i = 0 FOR n -- gather in the right number of elves BOOL any: SEQ a ? any -- let an elf in a.ack ? any -- wait for this elf to report its entry ping ! TRUE -- try to wake up Santa (enough elves are here) SEQ i = 0 FOR n -- let the elves leave the waiting room BOOL any: b ? any ping ! TRUE -- wait for Santa to greet all the elves : PROC reindeer (VAL INT id, seed, BARRIER just.reindeer, santa.reindeer, SHARED CHAN INT to.santa!, SHARED CHAN REINDEER.MSG report!) INITIAL INT my.seed IS seed: SEQ random.warm.up (5000, my.seed) WHILE TRUE SEQ CLAIM report ! holiday; id -- "I'm on holiday" + id random.wait (HOLIDAY.TIME, my.seed) -- sleep for random amount of time CLAIM report ! deer.ready; id -- "I'm back from holiday" + id SYNC just.reindeer -- wait for all deer to return CLAIM to.santa ! id -- send id and get harnessed SYNC santa.reindeer -- wait for others to be harnessed CLAIM report ! deliver; id -- "I'm delivering toys" + id SYNC santa.reindeer -- until Santa takes us all home CLAIM report ! deer.done; id -- "I'm back from sleigh run" + id CLAIM to.santa ! id -- get unharnessed : PROC elf (VAL INT id, seed, SHARED CHAN BOOL just.elves.a!, just.elves.a.ack!, just.elves.b!, SHARED CHAN BOOL santa.elves.a!, santa.elves.b!, SHARED CHAN INT to.santa!, SHARED CHAN ELF.MSG report!) INITIAL INT my.seed IS seed: SEQ random.warm.up (5000, my.seed) WHILE TRUE SEQ CLAIM report ! working; id -- "I'm working" + id random.wait (WORKING.TIME, my.seed) -- until I have a problem CLAIM report ! elf.ready; id -- "I want to see Santa" + id CLAIM just.elves.a ! TRUE -- let me into the waiting room CLAIM report ! waiting; id -- "I'm in the waiting room" + id CLAIM just.elves.a.ack ! TRUE -- you can let someone else in now CLAIM just.elves.b ! TRUE -- wait for enough elves to gather CLAIM to.santa ! id -- say hello to Santa sync (santa.elves.a!, santa.elves.b!) -- wait for others to say hello CLAIM report ! consult; id -- "I'm consulting Santa" + id sync (santa.elves.a!, santa.elves.b!) -- until Santa has had enough CLAIM report ! elf.done; id -- "I'm done consulting" + id CLAIM to.santa ! id -- say goodbye to Santa : PROC santa (VAL INT seed, CHAN INT from.reindeer?, BARRIER santa.reindeer, CHAN BOOL just.elves.ping?, CHAN INT from.elves?, SHARED CHAN BOOL santa.elves.a!, santa.elves.b!, SHARED CHAN SANTA.MSG report!) INITIAL INT my.seed IS seed: SEQ random.warm.up (5000, my.seed) WHILE TRUE PRI ALT INT id: from.reindeer ? id -- the first reindeer is here SEQ CLAIM report ! reindeer.ready -- "Ho, Ho, Ho, reindeer are here" CLAIM report ! harness; id -- "Harnessing reindeer " + id SEQ i = 0 FOR G.REINDEER - 1 -- for the remaining deer SEQ from.reindeer ? id -- receive their id CLAIM report ! harness; id -- "Harnessing reindeer " + id CLAIM report ! mush.mush -- "Mush Mush" SYNC santa.reindeer -- tell reindeer all are harnessed random.wait (DELIVERY.TIME, my.seed) -- deliver toys for some random time CLAIM report ! woah -- "Whoa ... let?s go home" SYNC santa.reindeer -- signal everyone to return home SEQ i = 0 FOR G.REINDEER -- for each deer from.reindeer ?? id -- receive their id CLAIM report ! unharness; id -- "Unharnessing reindeer " + id BOOL any: just.elves.ping ? any -- a party of elves is at door SEQ CLAIM report ! elves.ready -- "Ho, Ho, Ho, elves are here" SEQ i = 0 FOR G.ELVES -- for each elf in party INT id: -- (G.ELVES is size of party) SEQ from.elves ? id -- receive elf id CLAIM report ! greet; id -- "Hello elf " + id just.elves.ping ? any -- tell waiting room all have arrived CLAIM report ! consulting -- "Consulting with elves" sync (santa.elves.a!, santa.elves.b!) -- tell elf party all are here random.wait (CONSULTATION.TIME, my.seed) -- consult for a random time CLAIM report ! santa.done -- "Ok, all done - thanks!" sync (santa.elves.a!, santa.elves.b!) -- tell elves consultancy over SEQ i = 0 FOR G.ELVES -- for each elf in party INT id: from.elves ?? id -- receive elf id CLAIM report ! goodbye; id -- "Goodbye elf " + id : PROC santa.system (VAL INT seed, SHARED CHAN MESSAGE report!) BARRIER just.reindeer, santa.reindeer: SHARED ! CHAN INT reindeer.2.santa: SHARED ! CHAN BOOL just.elves.a, just.elves.b: -- extended partial barrier CHAN BOOL just.elves.ping: -- channels (just.elves) SHARED ! CHAN BOOL just.elves.a.ack: -- extended output (just.elves.a) SHARED ! CHAN BOOL santa.elves.a, santa.elves.b: -- partial barrier channels SHARED ! CHAN INT elves.2.santa: PAR PAR ENROLL santa.reindeer santa (seed + (N.REINDEER + N.ELVES), reindeer.2.santa?, santa.reindeer, just.elves.ping?, elves.2.santa?, santa.elves.a!, santa.elves.b!, report!) PAR i = 0 FOR N.REINDEER ENROLL just.reindeer, santa.reindeer reindeer (i, seed + i, just.reindeer, santa.reindeer, reindeer.2.santa!, report!) PAR i = 0 FOR N.ELVES elf (i, N.REINDEER + (seed + i), just.elves.a!, just.elves.a.ack!, just.elves.b!, santa.elves.a!, santa.elves.b!, elves.2.santa!, report!) waiting.room (G.ELVES, just.elves.a?, just.elves.a.ack?, just.elves.b?, just.elves.ping!) p.bar (G.ELVES + 1, santa.elves.a?, santa.elves.b?) : PROC santa.paper.6 (CHAN BYTE screen!) INT seed: SEQ random.initialise (seed) SHARED ! CHAN MESSAGE report: PAR santa.system (seed, report!) display (report?, screen!) :