f5f1490bc30bbeef66ff40f57d3ae644e49b9f2b
[model-checker-benchmarks.git] / mpmc-queue / note.txt
1 #1 Why this data structure is non-SC (but it's SC at abstraction).
2
3 The underlying pattern of the non-SCness are as the following:
4
5 T1                              T2
6 x = 1;                  y = 1;
7 r1 = y;                 r2 = x;
8
9 Suppose there are two identical threads, both having a writer followed by a
10 reader, as follows:
11
12 T1                                                      T2
13 m_written.CAS;                          m_rdwr.CAS;
14
15 m_rdwr.CAS;                                     m_written.CAS; // In write_publish()
16
17 m_written.load; // a            m_rdwr.load; // The first in the read_fetch() // b
18
19 a & b can both read old value and it's non-SC. However, the later loads and CAS
20 in the loops will finally fix this problem.
21
22
23
24 Run testcase1 with -Y, we got w3 & w7 to be acquire, and w4 & w8 release. Then
25 if we run testcase1 with -Y on its "-y" result, we will make other parameters
26 seq_cst.
27
28 However, we might have a bug in the model-checker when we ran with -y,
29 explanation as follows:
30
31 After we strengthen w1 & w6 to be sc, w1 can still read a value from a store
32 that is modification ordered before w6 (w6 is SC before w1). We should deal with
33 this after the OOPSLA deadline.