loading...
System State
Tutorial
POPL16
POPL17
Hand-written tests
More hand-written tests
Coherence
MP: Message Passing
LB: Load Buffering
SB: Store Buffer forwarding
PPO: Preserved Program Order
R
S
2+2W
RWC: Read to Write Causality
WRC: Write to Read Causality
WRR
WRW
WWC
ISA2: B cumulativity
3.2W
3.LB
3.SB
IRIW: Independent Reads of Independent Writes
IRRWIW
IRWIW
W+
Z6
POPL17
Hand-written tests
MP: Message Passing
LB: Load Buffering
SB: Store buffer forwarding
2+2W
R
S
ISA2: B cumulativity
RWC: Read to Write Causality
WRC: Write to Read Causality
WWC
IRIW: Independent Reads of Independent Writes
IRRWIW
IRWIW
PPO: Preserved Program Order
3.2W
3.LB
3.SB
WRR+2W
WRW+2W
W+RWC
WRW+WR
Z6.0
Z6.1
Z6.2
Z6.3
Z6.4
Z6.5
Model Options
PLDI11
Flowing
POP
NOP
Which transitions should be taken automatically by the tool:
none
the instruction-internal transitions
a larger set of transitions which we proved can be taken eagerly, without removing any observable behaviour
the above and additional believed-safe transitions
Tree speculation:
allow
forbid
ELF Options
Number of threads to create:
UI Options
full
compact
Prefer symbolic values
Print the final state values in hexadecimal
Generate
trace(s) by taking random transitions
Topology Choice for Flowing Model
Topology for two-thread tests
Topology for three-thread tests
Topology for four-thread tests