:orphan: ------------------------------------- Tutorial code trace (bufferSize == 5) ------------------------------------- .. code:: shell USER% ./mcmini -q -m117 -f ./subtle 5 About to exec into ./subtle TraceId 205, *** DEADLOCK DETECTED *** THREAD BACKTRACE 1. thread 0: starts 2. thread 0: pthread_mutex_init(mut:1, _) 3. thread 0: pthread_mutex_init(mut:2, _) 4. thread 0: pthread_mutex_init(mut:3, _) 5. thread 0: pthread_mutex_init(mut:4, _) 6. thread 0: pthread_cond_init(cond:1, _) 7. thread 0: pthread_cond_init(cond:2, _) 8. thread 0: pthread_create(thr:1, _, _, _) 9. thread 0: pthread_create(thr:2, _, _, _) 10. thread 1: starts 11. thread 1: pthread_mutex_lock(mut:1) 12. thread 1: pthread_mutex_unlock(mut:1) 13. thread 1: pthread_mutex_lock(mut:3) 14. thread 1: pthread_mutex_unlock(mut:3) 15. thread 1: pthread_mutex_lock(mut:4) 16. thread 1: pthread_mutex_unlock(mut:4) 17. thread 1: pthread_mutex_lock(mut:1) 18. thread 1: pthread_mutex_unlock(mut:1) 19. thread 1: pthread_mutex_lock(mut:2) 20. thread 1: pthread_cond_signal(cond:1) [Lost wakeup? (No thread waiting on cond) ] 21. thread 1: pthread_mutex_unlock(mut:2) 22. thread 1: pthread_mutex_lock(mut:1) 23. thread 1: pthread_mutex_unlock(mut:1) 24. thread 1: pthread_mutex_lock(mut:3) 25. thread 1: pthread_mutex_unlock(mut:3) 26. thread 1: pthread_mutex_lock(mut:4) 27. thread 1: pthread_mutex_unlock(mut:4) 28. thread 1: pthread_mutex_lock(mut:1) 29. thread 1: pthread_mutex_unlock(mut:1) 30. thread 1: pthread_mutex_lock(mut:2) 31. thread 1: pthread_cond_signal(cond:1) [Lost wakeup? (No thread waiting on cond) ] 32. thread 1: pthread_mutex_unlock(mut:2) 33. thread 1: pthread_mutex_lock(mut:1) 34. thread 1: pthread_mutex_unlock(mut:1) 35. thread 1: pthread_mutex_lock(mut:3) 36. thread 1: pthread_mutex_unlock(mut:3) 37. thread 1: pthread_mutex_lock(mut:4) 38. thread 1: pthread_mutex_unlock(mut:4) 39. thread 1: pthread_mutex_lock(mut:1) 40. thread 1: pthread_mutex_unlock(mut:1) 41. thread 1: pthread_mutex_lock(mut:2) 42. thread 1: pthread_cond_signal(cond:1) [Lost wakeup? (No thread waiting on cond) ] 43. thread 1: pthread_mutex_unlock(mut:2) 44. thread 1: pthread_mutex_lock(mut:1) 45. thread 1: pthread_mutex_unlock(mut:1) 46. thread 1: pthread_mutex_lock(mut:3) 47. thread 1: pthread_mutex_unlock(mut:3) 48. thread 1: pthread_mutex_lock(mut:4) 49. thread 1: pthread_mutex_unlock(mut:4) 50. thread 1: pthread_mutex_lock(mut:1) 51. thread 1: pthread_mutex_unlock(mut:1) 52. thread 1: pthread_mutex_lock(mut:2) 53. thread 1: pthread_cond_signal(cond:1) [Lost wakeup? (No thread waiting on cond) ] 54. thread 1: pthread_mutex_unlock(mut:2) 55. thread 1: pthread_mutex_lock(mut:1) 56. thread 1: pthread_mutex_unlock(mut:1) 57. thread 1: pthread_mutex_lock(mut:3) 58. thread 1: pthread_mutex_unlock(mut:3) 59. thread 1: pthread_mutex_lock(mut:4) 60. thread 1: pthread_mutex_unlock(mut:4) 61. thread 1: pthread_mutex_lock(mut:1) 62. thread 1: pthread_mutex_unlock(mut:1) 63. thread 1: pthread_mutex_lock(mut:2) 64. thread 1: pthread_cond_signal(cond:1) [Lost wakeup? (No thread waiting on cond) ] 65. thread 1: pthread_mutex_unlock(mut:2) 66. thread 1: pthread_mutex_lock(mut:1) 67. thread 1: pthread_mutex_unlock(mut:1) 68. thread 1: pthread_mutex_lock(mut:3) 69. thread 1: pthread_mutex_unlock(mut:3) 70. thread 1: pthread_mutex_lock(mut:4) 71. thread 1: pthread_cond_wait(cond:2, mut:4) (awake -> asleep) 72. thread 2: starts 73. thread 2: pthread_mutex_lock(mut:3) 74. thread 2: pthread_mutex_unlock(mut:3) 75. thread 2: pthread_mutex_lock(mut:1) 76. thread 2: pthread_mutex_unlock(mut:1) 77. thread 2: pthread_mutex_lock(mut:2) 78. thread 2: pthread_mutex_unlock(mut:2) 79. thread 2: pthread_mutex_lock(mut:3) 80. thread 2: pthread_mutex_unlock(mut:3) 81. thread 2: pthread_mutex_lock(mut:4) 82. thread 2: pthread_cond_signal(cond:2) 83. thread 2: pthread_mutex_unlock(mut:4) 84. thread 1: pthread_cond_wait(cond:2, mut:4) (asleep -> awake) 85. thread 1: pthread_mutex_lock(mut:3) 86. thread 1: pthread_mutex_unlock(mut:3) 87. thread 1: pthread_mutex_unlock(mut:4) 88. thread 1: pthread_mutex_lock(mut:1) 89. thread 1: pthread_mutex_unlock(mut:1) 90. thread 1: pthread_mutex_lock(mut:2) 91. thread 1: pthread_cond_signal(cond:1) [Lost wakeup? (No thread waiting on cond) ] 92. thread 1: pthread_mutex_unlock(mut:2) 93. thread 1: pthread_mutex_lock(mut:1) 94. thread 1: pthread_mutex_unlock(mut:1) 95. thread 1: pthread_mutex_lock(mut:3) 96. thread 1: pthread_mutex_unlock(mut:3) 97. thread 1: pthread_mutex_lock(mut:4) 98. thread 1: pthread_cond_wait(cond:2, mut:4) (awake -> asleep) 99. thread 2: pthread_mutex_lock(mut:3) 100. thread 2: pthread_mutex_unlock(mut:3) 101. thread 2: pthread_mutex_lock(mut:1) 102. thread 2: pthread_mutex_unlock(mut:1) 103. thread 2: pthread_mutex_lock(mut:2) 104. thread 2: pthread_mutex_unlock(mut:2) 105. thread 2: pthread_mutex_lock(mut:3) 106. thread 2: pthread_mutex_unlock(mut:3) 107. thread 2: pthread_mutex_lock(mut:4) 108. thread 2: pthread_cond_signal(cond:2) 109. thread 2: pthread_mutex_unlock(mut:4) 110. thread 1: pthread_cond_wait(cond:2, mut:4) (asleep -> awake) 111. thread 1: pthread_mutex_lock(mut:3) 112. thread 1: pthread_mutex_unlock(mut:3) 113. thread 1: pthread_mutex_unlock(mut:4) 114. thread 1: pthread_mutex_lock(mut:1) 115. thread 1: pthread_mutex_unlock(mut:1) 116. thread 1: pthread_mutex_lock(mut:2) 117. thread 1: pthread_cond_signal(cond:1) [Lost wakeup? (No thread waiting on cond) ] 118. thread 1: pthread_mutex_unlock(mut:2) 119. thread 1: pthread_mutex_lock(mut:1) 120. thread 1: pthread_mutex_unlock(mut:1) 121. thread 1: pthread_mutex_lock(mut:3) 122. thread 1: pthread_mutex_unlock(mut:3) 123. thread 1: pthread_mutex_lock(mut:4) 124. thread 1: pthread_cond_wait(cond:2, mut:4) (awake -> asleep) 125. thread 2: pthread_mutex_lock(mut:3) 126. thread 2: pthread_mutex_unlock(mut:3) 127. thread 2: pthread_mutex_lock(mut:1) 128. thread 2: pthread_mutex_unlock(mut:1) 129. thread 2: pthread_mutex_lock(mut:2) 130. thread 2: pthread_mutex_unlock(mut:2) 131. thread 2: pthread_mutex_lock(mut:3) 132. thread 2: pthread_mutex_unlock(mut:3) 133. thread 2: pthread_mutex_lock(mut:4) 134. thread 2: pthread_cond_signal(cond:2) 135. thread 2: pthread_mutex_unlock(mut:4) 136. thread 1: pthread_cond_wait(cond:2, mut:4) (asleep -> awake) 137. thread 1: pthread_mutex_lock(mut:3) 138. thread 1: pthread_mutex_unlock(mut:3) 139. thread 1: pthread_mutex_unlock(mut:4) 140. thread 1: pthread_mutex_lock(mut:1) 141. thread 1: pthread_mutex_unlock(mut:1) 142. thread 1: pthread_mutex_lock(mut:2) 143. thread 1: pthread_cond_signal(cond:1) [Lost wakeup? (No thread waiting on cond) ] 144. thread 1: pthread_mutex_unlock(mut:2) 145. thread 1: pthread_mutex_lock(mut:1) 146. thread 1: pthread_mutex_unlock(mut:1) 147. thread 1: pthread_mutex_lock(mut:3) 148. thread 1: pthread_mutex_unlock(mut:3) 149. thread 1: pthread_mutex_lock(mut:4) 150. thread 1: pthread_cond_wait(cond:2, mut:4) (awake -> asleep) 151. thread 2: pthread_mutex_lock(mut:3) 152. thread 2: pthread_mutex_unlock(mut:3) 153. thread 2: pthread_mutex_lock(mut:1) 154. thread 2: pthread_mutex_unlock(mut:1) 155. thread 2: pthread_mutex_lock(mut:2) 156. thread 2: pthread_mutex_unlock(mut:2) 157. thread 2: pthread_mutex_lock(mut:3) 158. thread 2: pthread_mutex_unlock(mut:3) 159. thread 2: pthread_mutex_lock(mut:4) 160. thread 2: pthread_cond_signal(cond:2) 161. thread 2: pthread_mutex_unlock(mut:4) 162. thread 1: pthread_cond_wait(cond:2, mut:4) (asleep -> awake) 163. thread 1: pthread_mutex_lock(mut:3) 164. thread 1: pthread_mutex_unlock(mut:3) 165. thread 1: pthread_mutex_unlock(mut:4) 166. thread 1: pthread_mutex_lock(mut:1) 167. thread 1: pthread_mutex_unlock(mut:1) 168. thread 1: pthread_mutex_lock(mut:2) 169. thread 1: pthread_cond_signal(cond:1) [Lost wakeup? (No thread waiting on cond) ] 170. thread 1: pthread_mutex_unlock(mut:2) 171. thread 1: pthread_mutex_lock(mut:1) 172. thread 1: pthread_mutex_unlock(mut:1) 173. thread 1: pthread_mutex_lock(mut:3) 174. thread 1: pthread_mutex_unlock(mut:3) 175. thread 2: pthread_mutex_lock(mut:3) 176. thread 2: pthread_mutex_unlock(mut:3) 177. thread 2: pthread_mutex_lock(mut:1) 178. thread 2: pthread_mutex_unlock(mut:1) 179. thread 2: pthread_mutex_lock(mut:2) 180. thread 2: pthread_mutex_unlock(mut:2) 181. thread 2: pthread_mutex_lock(mut:3) 182. thread 2: pthread_mutex_unlock(mut:3) 183. thread 2: pthread_mutex_lock(mut:4) 184. thread 2: pthread_cond_signal(cond:2) [Lost wakeup? (No thread waiting on cond) ] 185. thread 2: pthread_mutex_unlock(mut:4) 186. thread 2: pthread_mutex_lock(mut:3) 187. thread 2: pthread_mutex_unlock(mut:3) 188. thread 2: pthread_mutex_lock(mut:1) 189. thread 2: pthread_mutex_unlock(mut:1) 190. thread 2: pthread_mutex_lock(mut:2) 191. thread 2: pthread_mutex_unlock(mut:2) 192. thread 2: pthread_mutex_lock(mut:3) 193. thread 2: pthread_mutex_unlock(mut:3) 194. thread 2: pthread_mutex_lock(mut:4) 195. thread 2: pthread_cond_signal(cond:2) [Lost wakeup? (No thread waiting on cond) ] 196. thread 2: pthread_mutex_unlock(mut:4) 197. thread 2: pthread_mutex_lock(mut:3) 198. thread 2: pthread_mutex_unlock(mut:3) 199. thread 2: pthread_mutex_lock(mut:1) 200. thread 2: pthread_mutex_unlock(mut:1) 201. thread 2: pthread_mutex_lock(mut:2) 202. thread 2: pthread_mutex_unlock(mut:2) 203. thread 2: pthread_mutex_lock(mut:3) 204. thread 2: pthread_mutex_unlock(mut:3) 205. thread 2: pthread_mutex_lock(mut:4) 206. thread 2: pthread_cond_signal(cond:2) [Lost wakeup? (No thread waiting on cond) ] 207. thread 2: pthread_mutex_unlock(mut:4) 208. thread 2: pthread_mutex_lock(mut:3) 209. thread 2: pthread_mutex_unlock(mut:3) 210. thread 2: pthread_mutex_lock(mut:1) 211. thread 2: pthread_mutex_unlock(mut:1) 212. thread 2: pthread_mutex_lock(mut:2) 213. thread 2: pthread_mutex_unlock(mut:2) 214. thread 2: pthread_mutex_lock(mut:3) 215. thread 2: pthread_mutex_unlock(mut:3) 216. thread 2: pthread_mutex_lock(mut:4) 217. thread 2: pthread_cond_signal(cond:2) [Lost wakeup? (No thread waiting on cond) ] 218. thread 2: pthread_mutex_unlock(mut:4) 219. thread 2: pthread_mutex_lock(mut:3) 220. thread 2: pthread_mutex_unlock(mut:3) 221. thread 2: pthread_mutex_lock(mut:1) 222. thread 2: pthread_mutex_unlock(mut:1) 223. thread 2: pthread_mutex_lock(mut:2) 224. thread 2: pthread_mutex_unlock(mut:2) 225. thread 2: pthread_mutex_lock(mut:3) 226. thread 2: pthread_mutex_unlock(mut:3) 227. thread 2: pthread_mutex_lock(mut:4) 228. thread 2: pthread_cond_signal(cond:2) [Lost wakeup? (No thread waiting on cond) ] 229. thread 2: pthread_mutex_unlock(mut:4) 230. thread 1: pthread_mutex_lock(mut:4) 231. thread 1: pthread_cond_wait(cond:2, mut:4) (awake -> asleep) 232. thread 2: pthread_mutex_lock(mut:3) 233. thread 2: pthread_mutex_unlock(mut:3) 234. thread 2: pthread_mutex_lock(mut:1) 235. thread 2: pthread_mutex_unlock(mut:1) 236. thread 2: pthread_mutex_lock(mut:2) 237. thread 2: pthread_cond_wait(cond:1, mut:2) (awake -> asleep) 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 1, 2, 2, 2, 2, 2, 2, END THREAD PENDING OPERATIONS * thread 0: pthread_join(thr:1, _) [ Blocked ] thread 1: pthread_cond_wait(cond:2, mut:4) (asleep -> awake) [ Blocked ] thread 2: pthread_cond_wait(cond:1, mut:2) (asleep -> awake) [ Blocked ] END ***** Model checking completed! ***** *** DEADLOCK DETECTED *** (Trace number (traceId): 205) Number of traces: 206 Total number of transitions: 1107 Elapsed time: 5 seconds