~james/reorder

2
main
main
reorder/cases/peterson.sexp -rw-r--r--452 bytes ViewLogBlameView rawPermalink 908ea7335d feat(core): initialise tso checking and fence synthesis 29 days ago
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
(case
  (name "Peterson mutual exclusion")
  (names flag0 flag1 turn)
  (bound 14)
  (threads
    ((store 0 1)
     (store 2 1)
     (load 1 0)
     (branch 0 0 6)
     (load 2 1)
     (branch 1 1 2)
     (enter)
     (leave)
     (store 0 0))
    ((store 1 1)
     (store 2 0)
     (load 0 0)
     (branch 0 0 6)
     (load 2 1)
     (branch 1 0 2)
     (enter)
     (leave)
     (store 1 0)))
  (candidates (0 1) (0 2) (1 1) (1 2))
  (goal overlap))