# # Hermann Kopetz and J. Reisinger. The non-blocking write protocol # nbw: A solution to a real-time synchronisation problem. In IEEE Real- # Time Systems Symposium’93, pages 131–137, 1993. # # Writer, Writer-Reader. # # IS NOT robust. # # Memory layout: # 0 — buf # 1 — counter thread writer initial w0 transition w0 w0_1 local buf 0 transition w0_1 w1 local counter 1 transition w1 w2 read cnt counter transition w2 w3 write + cnt 1 counter transition w3 w4 write 666 buf transition w4 w5 write + cnt 2 counter end thread writerreader initial w0 transition w0 w0_1 local buf 0 transition w0_1 w1 local counter 1 transition w1 w2 read cnt counter transition w2 w3 write + cnt 1 counter transition w3 w4 write 666 buf transition w4 r0 write + cnt 2 counter transition r0 r0_1 local buf 0 transition r0_1 r1 local counter 1 transition r1 r2 read cnt_b counter transition r2 r3 read value buf transition r3 r4 read cnt_e counter transition r4 r0 check || != cnt_b cnt_e == & cnt_b 1 1 transition r4 r5 check && == cnt_b cnt_e == & cnt_b 1 0 end