semaphore.p 2.4 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183
  1. /*
  2. spin -a semaphore.p
  3. pcc -DSAFETY -DREACH -DMEMLIM'='500 -o pan pan.c
  4. pan -i
  5. rm pan.* pan
  6. */
  7. #define N 3
  8. bit listlock;
  9. byte value;
  10. bit onlist[N];
  11. bit waiting[N];
  12. bit sleeping[N];
  13. bit acquired[N];
  14. inline lock(x)
  15. {
  16. atomic { x == 0; x = 1 }
  17. }
  18. inline unlock(x)
  19. {
  20. assert x==1;
  21. x = 0
  22. }
  23. inline sleep(cond)
  24. {
  25. assert !sleeping[_pid];
  26. assert !interrupted;
  27. if
  28. :: cond
  29. :: atomic { else -> sleeping[_pid] = 1 } ->
  30. !sleeping[_pid]
  31. fi;
  32. if
  33. :: skip
  34. :: interrupted = 1
  35. fi
  36. }
  37. inline wakeup(id)
  38. {
  39. if
  40. :: sleeping[id] == 1 -> sleeping[id] = 0
  41. :: else
  42. fi
  43. }
  44. inline semqueue()
  45. {
  46. lock(listlock);
  47. assert !onlist[_pid];
  48. onlist[_pid] = 1;
  49. unlock(listlock)
  50. }
  51. inline semdequeue()
  52. {
  53. lock(listlock);
  54. assert onlist[_pid];
  55. onlist[_pid] = 0;
  56. waiting[_pid] = 0;
  57. unlock(listlock)
  58. }
  59. inline semwakeup(n)
  60. {
  61. byte i, j;
  62. lock(listlock);
  63. i = 0;
  64. j = n;
  65. do
  66. :: (i < N && j > 0) ->
  67. if
  68. :: onlist[i] && waiting[i] ->
  69. atomic { printf("kicked %d\n", i);
  70. waiting[i] = 0 };
  71. wakeup(i);
  72. j--
  73. :: else
  74. fi;
  75. i++
  76. :: else -> break
  77. od;
  78. /* reset i and j to reduce state space */
  79. i = 0;
  80. j = 0;
  81. unlock(listlock)
  82. }
  83. inline semrelease(n)
  84. {
  85. atomic { value = value+n; printf("release %d\n", n); };
  86. semwakeup(n)
  87. }
  88. inline canacquire()
  89. {
  90. atomic { value > 0 -> value--; };
  91. acquired[_pid] = 1
  92. }
  93. #define semawoke() !waiting[_pid]
  94. inline semacquire(block)
  95. {
  96. if
  97. :: atomic { canacquire() -> printf("easy acquire\n"); } ->
  98. goto out
  99. :: else
  100. fi;
  101. if
  102. :: !block -> goto out
  103. :: else
  104. fi;
  105. semqueue();
  106. do
  107. :: skip ->
  108. waiting[_pid] = 1;
  109. if
  110. :: atomic { canacquire() -> printf("hard acquire\n"); } ->
  111. break
  112. :: else
  113. fi;
  114. sleep(semawoke())
  115. if
  116. :: interrupted ->
  117. printf("%d interrupted\n", _pid);
  118. break
  119. :: !interrupted
  120. fi
  121. od;
  122. semdequeue();
  123. if
  124. :: !waiting[_pid] ->
  125. semwakeup(1)
  126. :: else
  127. fi;
  128. out:
  129. assert (!block || interrupted || acquired[_pid]);
  130. assert !(interrupted && acquired[_pid]);
  131. assert !waiting[_pid];
  132. printf("%d done\n", _pid);
  133. }
  134. active[N] proctype acquire()
  135. {
  136. bit interrupted;
  137. semacquire(1);
  138. printf("%d finished\n", _pid);
  139. skip
  140. }
  141. active proctype release()
  142. {
  143. byte k;
  144. k = 0;
  145. do
  146. :: k < N ->
  147. semrelease(1);
  148. k++;
  149. :: else -> break
  150. od;
  151. skip
  152. }
  153. /*
  154. * If this guy, the highest-numbered proc, sticks
  155. * around, then everyone else sticks around.
  156. * This makes sure that we get a state line for
  157. * everyone in a proc dump.
  158. */
  159. active proctype dummy()
  160. {
  161. end: 0;
  162. }