| | 106 | For each shared variable `v` introduce a second variable `v_state`. The type of `v_state` is obtained from the type of `v` by replacing all primitive types (leaf nodes in the type tree) by `int`. Initially all these ints are -1. |
| | 107 | |
| | 108 | A write to (some part of) the shared variable by thread tid: |
| | 109 | * if the state value is -1, set it to tid, then do the write |
| | 110 | * if the state value is tid, do the write |
| | 111 | * else report a data race. |
| | 112 | |
| | 113 | A read from (some part of) the shared variable by thread tid: |
| | 114 | * if the state value is -1 or tid, do the read |
| | 115 | * else report a data race. |
| | 116 | |
| | 117 | Translating `flush`of (some part of) the shared variable by thread tid: |
| | 118 | * if the state value is -1: no-op |
| | 119 | * if the state value is tid: set it to -1 |
| | 120 | * else: some other thread has some write to the variable which it hasn't flushed. Not exactly sure what is supposed to happen, but I think this is like a race condition |
| | 121 | |
