# Distributed Dining Philosophers. Based on the example in Section 13.3 of # "The SR Programming Language: Concurrency in Practice", by Greg Andrews and # Ron Olsson, Benjamin/Cummings, 1993. The algorithm is from Chandy and Misra, # "Drinking Philosophers Problem", ACM TOPLAS v 6, n 4, Oct 1984, pp 632-646. # Usage: a.out [n secs t_secs e_secs t_secs e_secs ...] # (for n philosophers, secs seconds running time, t_secs max thinking seconds, # e_secs max eating seconds for each philosopher) # # Modified for xtango's animator interpreter. All normal SR simulation output # is done with write, and all xtango animator commands are output with printf. # resource Philosopher import Servant body Philosopher(myservant : cap Servant; id, thinking, eating: int) process phil do true -> nap(int(random(thinking))) printf("comment "); write(age(), "philosopher", id, "is hungry") ##### animator #####v # Change a hungry philosopher's symbol to be solid green. printf("color %d green\n", id); printf("fill %d solid\n", id) ##### animator #####^ myservant.getforks() ##### animator #####v # Change an eating philosopher's symbol to be solid blue. printf("color %d blue\n", id) ##### animator #####^ nap(int(random(eating))) ##### animator #####v # Change a thinking philosopher's symbol to an outline black circle. printf("fill %d outline\n", id); printf("color %d black\n", id) ##### animator #####^ myservant.relforks() od end phil end Philosopher resource Servant op getforks(), relforks() op needR(), needL(), passR(), passL() op links(r, l : cap Servant) op forks(haveR, dirtyR, haveL, dirtyL : bool) ##### animator #####v # This op and the variables below are used to hold the symbol id numbers of # the left and right fork symbols and where the left and right forks are # placed next to the philosopher when it possesses them. op fork_ids(forkR, forkL, holderR, holderL : int) ##### animator #####^ body Servant(id : int) op hungry(), eat() var r, l : cap Servant var haveR, dirtyR, haveL, dirtyL : bool ##### animator #####v var forkR, forkL, holderR, holderL : int ##### animator #####^ proc getforks() send hungry(); receive eat() end process server receive links(r, l) receive forks(haveR, dirtyR, haveL, dirtyL) ##### animator #####v # Move a left or right fork initially given to this philosopher to be next # to the philosopher. receive fork_ids(forkR, forkL, holderR, holderL) if haveR -> printf("jumpto %d %d\n", forkR, holderR) fi if haveL -> printf("jumpto %d %d\n", forkL, holderL) fi if dirtyR -> printf("color %d orange\n", forkR) printf("fill %d solid\n", forkR) fi if dirtyL -> printf("color %d orange\n", forkL) printf("fill %d solid\n", forkL) fi ##### animator #####^ do true-> in hungry() -> if ~haveR -> send r.needL() [] else -> printf("comment ") write(age(), "philosopher", id, "has right fork") fi if ~haveL -> send l.needR() [] else -> printf("comment ") write(age(), "philosopher", id, "has left fork") fi do ~(haveR & haveL) -> in passR() -> haveR := true; dirtyR := false printf("comment ") write(age(), "philosopher", id, "got right fork") ##### animator #####v # Move the fork from where it was to be next to this philosopher and then # change its symbol to be a black outline circle i.e. not dirty. Also raise # the fork's symbol to the closest viewing plane to make it more visible. printf("moveto %d %d\n", forkR, holderR) printf("fill %d outline\n", forkR) printf("color %d black\n", forkR) printf("raise %d\n", forkR) ##### animator #####^ [] passL() -> haveL := true; dirtyL := false printf("comment ") write(age(), "philosopher", id, "got left fork") ##### animator #####v # Ditto. printf("moveto %d %d\n", forkL, holderL) printf("fill %d outline\n", forkL) printf("color %d black\n", forkL) printf("raise %d\n", forkL) ##### animator #####^ [] needR() st dirtyR -> haveR := false; dirtyR := false send r.passL(); send r.needL() printf("comment ") write(age(), "philosopher", id, "sends dirty right fork") [] needL() st dirtyL -> haveL := false; dirtyL := false send l.passR(); send l.needR() printf("comment ") write(age(), "philosopher", id, "sends dirty left fork") ni od printf("comment ") write(age(), "philosopher", id, "has both forks") send eat(); dirtyR := true; dirtyL := true receive relforks() printf("comment ") write(age(), "philosopher", id, "is finished eating") ##### animator #####v # Now that the philosopher has finished eating, its forks are dirty so # change their symbols to be solid orange circles. printf("color %d orange\n", forkL) printf("fill %d solid\n", forkL) printf("color %d orange\n", forkR) printf("fill %d solid\n", forkR) ##### animator #####^ [] needR() -> haveR := false; dirtyR := false; send r.passL() printf("comment ") write(age(), "philosopher", id, "sends right fork") [] needL() -> haveL := false; dirtyL := false; send l.passR() printf("comment ") write(age(), "philosopher", id, "sends left fork") ni od end server end Servant resource Main() import Philosopher, Servant var n := 5; getarg(1, n); var runtime := 60; getarg(2, runtime) var s[1:n] : cap Servant; var p[1:n] : cap Philosopher var think[1:n] : int := ([n] 5); var eat[1:n] : int := ([n] 2) fa i := 1 to n -> getarg(2*i+1, think[i]); getarg(2*i+2, eat[i]) af printf("comment "); write(n, "philosophers; think, eat times in seconds:") printf("comment "); fa i := 1 to n -> writes(" ", think[i]) af; write() printf("comment "); fa i := 1 to n -> writes(" ", eat[i]) af; write() ##### animator #####v # Change coordinates so 0,0 is the center, then create a big black outline # circle to be the table. printf("coords -1.5 -1.5 1.5 1.5\n") printf("circle 1000 0.0 0.0 1.0 black outline\n") # Put some annotated symbols on the screen. printf("circle 1001 -1.4 -0.6 0.02 black outline\n") printf("text 1002 -1.3 -0.625 0 black clean fork\n") printf("circle 1003 -1.4 -0.8 0.02 orange solid\n") printf("text 1004 -1.3 -0.825 0 black dirty fork\n") printf("circle 1005 -1.4 -1.0 0.05 black outline\n") printf("text 1006 -1.3 -1.025 0 black THINKING\n") printf("circle 1007 -1.4 -1.2 0.05 green solid\n") printf("text 1008 -1.3 -1.225 0 black HUNGRY\n") printf("circle 1009 -1.4 -1.4 0.05 blue solid\n") printf("text 1010 -1.3 -1.425 0 black EATING\n") # Put a clean set of forks, small black outline circles, near the table. printf("text 1011 %7.2f -1.41 0 black forks\n", -1.0+0.05*(n+1)) fa i := 1 to n -> printf("circle %d %7.2f -1.4 0.02 black outline\n", 3000+i-1, -1.0+0.05*i) af const TWO_PI := 2.0*acos(-1.0) fa i := 1 to n -> # Put the philosophers, black outline circles, around the table. printf("circle %d %7.2f %7.2f 0.1 black outline\n", i, sin(i*(TWO_PI/n)), cos(i*(TWO_PI/n))) # Number the philosophers. printf("text %d %7.2f %7.2f 1 black %d\n", 2000+i, sin(i*(TWO_PI/n))+0.1, cos(i*(TWO_PI/n))+0.1, i) # Put nearly invisible circles (points) on the left and right side of each # philosopher to be places the forks can be moved to when the philosopher # gets possession of a fork. printf("circle %d %7.2f %7.2f 0.001 black outline\n", 4000+2*i, sin(i*(TWO_PI/n)-0.12), cos(i*(TWO_PI/n)-0.13)) printf("circle %d %7.2f %7.2f 0.001 black outline\n", 4000+2*i+1, sin(i*(TWO_PI/n)+0.12), cos(i*(TWO_PI/n)+0.13)) af ##### animator #####^ fa i := 1 to n -> s[i] := create Servant(i) create Philosopher(s[i], i, 1000*think[i], 1000*eat[i]) af fa i := 1 to n -> send s[i].links(s[((i-2) mod n)+1], s[(i mod n)+1]) af send s[1].forks(true, true, true, true) fa i := 2 to n-1 -> send s[i].forks(false, false, true, false) af send s[n].forks(false, false, false, false) ##### animator #####v # Send to each philosopher the xtango animator symbol id's of the two forks # the philosopher needs to eat and the places where possessed forks are to # be moved next to the philosopher. fa i := 1 to n -> send s[i].fork_ids(3000+((i-1) mod n), 3000+(i mod n), 4000+2*i, 4000+2*i+1) af ##### animator #####^ nap(1000*runtime); printf("comment "); write("must stop now"); stop end Main /* ............... Example compile and run(s) % sr -o didp didp.sr % ./didp 5 10 | animator Press RUN ANIMATION button to begin XTANGO Version 1.52 5 philosophers; think, eat times in seconds: 5 5 5 5 5 2 2 2 2 2 632 philosopher 5 is hungry 634 philosopher 4 sends left fork 635 philosopher 1 sends right fork 636 philosopher 5 got right fork 639 philosopher 5 got left fork 641 philosopher 5 has both forks 1790 philosopher 5 is finished eating 2993 philosopher 4 is hungry 2996 philosopher 3 sends left fork 2997 philosopher 5 sends right fork 2998 philosopher 4 got right fork 3000 philosopher 4 got left fork 3003 philosopher 4 has both forks 3201 philosopher 3 is hungry 3204 philosopher 2 sends left fork 3205 philosopher 3 got right fork 3469 philosopher 1 is hungry 3471 philosopher 1 has left fork 3472 philosopher 5 sends left fork 3473 philosopher 1 got right fork 3476 philosopher 1 has both forks 4252 philosopher 1 is finished eating 4985 philosopher 4 is finished eating 4987 philosopher 4 sends right fork 4989 philosopher 3 got left fork 4991 philosopher 3 has both forks 5242 philosopher 2 is hungry 5277 philosopher 1 sends left fork 5279 philosopher 2 got right fork 7559 philosopher 3 is finished eating 7562 philosopher 3 sends right fork 7564 philosopher 4 is hungry 7565 philosopher 1 is hungry 7567 philosopher 5 is hungry 7569 philosopher 2 got left fork 7571 philosopher 2 has both forks 7572 philosopher 4 has left fork 7573 philosopher 1 has right fork 7576 philosopher 3 sends left fork 7577 philosopher 4 sends dirty left fork 7578 philosopher 4 got right fork 7580 philosopher 1 sends dirty right fork 7581 philosopher 5 got right fork 7584 philosopher 5 got left fork 7586 philosopher 5 has both forks 7915 philosopher 2 is finished eating 7917 philosopher 2 sends right fork 7918 philosopher 1 got left fork 8171 philosopher 5 is finished eating 8186 philosopher 5 sends right fork 8196 philosopher 5 sends left fork 8203 philosopher 4 got left fork 8215 philosopher 4 has both forks 8221 philosopher 1 got right fork 8246 philosopher 1 has both forks 8364 philosopher 2 is hungry 8366 philosopher 2 has left fork 9127 philosopher 1 is finished eating 9134 philosopher 1 sends left fork 9135 philosopher 2 got right fork 9137 philosopher 2 has both forks 9441 philosopher 5 is hungry 9443 philosopher 1 sends right fork 9444 philosopher 5 got left fork 9501 philosopher 4 is finished eating 9503 philosopher 4 sends left fork 9505 philosopher 5 got right fork 9507 philosopher 5 has both forks 9837 philosopher 2 is finished eating 9890 philosopher 3 is hungry 9893 philosopher 2 sends left fork 9894 philosopher 4 sends right fork 9895 philosopher 3 got right fork 9897 philosopher 3 got left fork 9906 philosopher 3 has both forks must stop now */