Skip to content

Instantly share code, notes, and snippets.

@dfyz
Last active May 7, 2023 18:51
Show Gist options
  • Save dfyz/292db5d09acb8be2d999d8b32c236d49 to your computer and use it in GitHub Desktop.
Save dfyz/292db5d09acb8be2d999d8b32c236d49 to your computer and use it in GitHub Desktop.
Modeling incorrect SPSC ring buffer
AArch64 RB.correct
"
Theoretical results:
States 2
1:X6=0; 1:X9=61;
1:X6=1; 1:X9=41;
"
{
0:X3=x; 0:X4=y; 0:X5=z;
1:X3=x; 1:X4=y; 1:X5=z;
}
P0 | P1 ;
LDAR W0, [X3] | MOV W9, #61 ;
LDR W1, [X4] | LDR W0, [X3] ;
CMP W0, W1 | LDAR W1, [X4] ;
B.NE skip1 | CMP W0, W1 ;
MOV W6, #41 | B.EQ skip ;
STR W6, [X5] | LDR W9, [X5] ;
MOV W6, #1 | MOV W6, #1 ;
STLR W6, [X4] | STLR W6, [X3] ;
skip1: | skip: ;
LDAR W0, [X3] | ;
LDR W1, [X4] | ;
CMP W0, W1 | ;
B.NE skip2 | ;
MOV W6, #42 | ;
STR W6, [X5] | ;
MOV W6, #2 | ;
STLR W6, [X4] | ;
skip2: | ;
exists (1:X6=1 /\ 1:X9=41)
AArch64 RB.head_rel
"
Theoretical results:
States 3
1:X6=0; 1:X9=61;
1:X6=1; 1:X9=41;
1:X6=1; 1:X9=42;
"
{
0:X3=x; 0:X4=y; 0:X5=z;
1:X3=x; 1:X4=y; 1:X5=z;
}
P0 | P1 ;
LDR W0, [X3] | MOV W9, #61 ;
LDR W1, [X4] | LDR W0, [X3] ;
CMP W0, W1 | LDAR W1, [X4] ;
B.NE skip1 | CMP W0, W1 ;
MOV W6, #41 | B.EQ skip ;
STR W6, [X5] | LDR W9, [X5] ;
MOV W6, #1 | MOV W6, #1 ;
STLR W6, [X4] | STR W6, [X3] ;
skip1: | skip: ;
LDR W0, [X3] | ;
LDR W1, [X4] | ;
CMP W0, W1 | ;
B.NE skip2 | ;
MOV W6, #42 | ;
STR W6, [X5] | ;
MOV W6, #2 | ;
STLR W6, [X4] | ;
skip2: | ;
exists (1:X6=1 /\ 1:X9=42)
AArch64 RB.head_rel.tail_rel
"
Theoretical results:
States 4
1:X6=0; 1:X9=61;
1:X6=1; 1:X9=0;
1:X6=1; 1:X9=41;
1:X6=1; 1:X9=42;
"
{
0:X3=x; 0:X4=y; 0:X5=z;
1:X3=x; 1:X4=y; 1:X5=z;
}
P0 | P1 ;
LDR W0, [X3] | MOV W9, #61 ;
LDR W1, [X4] | LDR W0, [X3] ;
CMP W0, W1 | LDR W1, [X4] ;
B.NE skip1 | CMP W0, W1 ;
MOV W6, #41 | B.EQ skip ;
STR W6, [X5] | LDR W9, [X5] ;
MOV W6, #1 | MOV W6, #1 ;
STR W6, [X4] | STR W6, [X3] ;
skip1: | skip: ;
LDR W0, [X3] | ;
LDR W1, [X4] | ;
CMP W0, W1 | ;
B.NE skip2 | ;
MOV W6, #42 | ;
STR W6, [X5] | ;
MOV W6, #2 | ;
STR W6, [X4] | ;
skip2: | ;
exists (1:X6=1 /\ 1:X9=0)
/* http://svr-pes20-cppmem.cl.cam.ac.uk/cppmem/ */
int main() {
atomic_int head = 0;
atomic_int tail = 0;
atomic_int data = 0;
{{{
{
r1 = head.load(memory_order_relaxed).readsvalue(0);
r2 = tail.load(memory_order_relaxed).readsvalue(0);
data.store(41, memory_order_relaxed);
tail.store(1, memory_order_release);
r3 = head.load(memory_order_relaxed).readsvalue(1);
r4 = tail.load(memory_order_relaxed).readsvalue(1);
data.store(42, memory_order_relaxed);
tail.store(2, memory_order_release);
}
|||
{
r1 = head.load(memory_order_relaxed).readsvalue(0);
r2 = tail.load(memory_order_acquire).readsvalue(1);
r3 = data.load(memory_order_relaxed);
head.store(1, memory_order_relaxed);
}
}}}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment