Current differences from CPPMem:
- The test suite does not use non-atomic initialisation yet.
- Use the "nonatomic" memory order to write non-atomic accesses.
- The default memory order is relaxed rather than SC.
- There is no need to declare variables.
- The tool works with Chrome, Firefox and Safari.
- This tool is under active development. Email us with any questions.
Click to reveal grammar guide.
LITMUS ::= CONFIG %% PROGRAM
| CONFIG %% PROGRAM %% ASSERTION
CONFIG ::= name= QUOTED_STRING NEWLINE values={ COMMA_SEPARATED(INT) }
REGISTER ::= r['a'-'z' 'A'-'Z' '0'-'9']*
GLOBAL ::= ['a'-'q' 's'-'z' 'A'-'Z']['a'-'z' 'A'-'Z' '0'-'9']*
THREAD ::= { PROGRAM }
EXPR ::= INT | REGISTER
B_EXPR ::= EXPR = EXPR
| EXPR > EXPR
| EXPR >= EXPR
| EXPR < EXPR
| EXPR <= EXPR
| B_EXPR && B_EXPR
| B_EXPR || B_EXPR
| ( B_EXPR )
| ! B_EXPR
MEMORY_ORDER ::= nonatomic | na
| relaxed | rlx
| release | rel
| acquire | acq
| sequentially_consistent | sc
PROGRAM ::= THREAD ||| THREAD
| PROGRAM ; PROGRAM
| GLOBAL := EXPR
| GLOBAL.store( EXPR , MEMORY_ORDER )
| REGISTER := GLOBAL
| REGISTER := GLOBAL.load( MEMORY_ORDER )
| if( B_EXPR ) { PROGRAM }
| if( B_EXPR ) { PROGRAM } else { PROGRAM }
| fence( MEMORY_ORDER )
OUTCOME ::= allow | forbid
ASSERTION ::= OUTCOME B_EXPR [ STRING = OUTCOME ]
| OUTCOME B_EXPR [ STRING = OUTCOME ] QUOTED_STRING
| CONFIG %% PROGRAM %% ASSERTION
CONFIG ::= name= QUOTED_STRING NEWLINE values={ COMMA_SEPARATED(INT) }
REGISTER ::= r['a'-'z' 'A'-'Z' '0'-'9']*
GLOBAL ::= ['a'-'q' 's'-'z' 'A'-'Z']['a'-'z' 'A'-'Z' '0'-'9']*
THREAD ::= { PROGRAM }
EXPR ::= INT | REGISTER
B_EXPR ::= EXPR = EXPR
| EXPR > EXPR
| EXPR >= EXPR
| EXPR < EXPR
| EXPR <= EXPR
| B_EXPR && B_EXPR
| B_EXPR || B_EXPR
| ( B_EXPR )
| ! B_EXPR
MEMORY_ORDER ::= nonatomic | na
| relaxed | rlx
| release | rel
| acquire | acq
| sequentially_consistent | sc
PROGRAM ::= THREAD ||| THREAD
| PROGRAM ; PROGRAM
| GLOBAL := EXPR
| GLOBAL.store( EXPR , MEMORY_ORDER )
| REGISTER := GLOBAL
| REGISTER := GLOBAL.load( MEMORY_ORDER )
| if( B_EXPR ) { PROGRAM }
| if( B_EXPR ) { PROGRAM } else { PROGRAM }
| fence( MEMORY_ORDER )
OUTCOME ::= allow | forbid
ASSERTION ::= OUTCOME B_EXPR [ STRING = OUTCOME ]
| OUTCOME B_EXPR [ STRING = OUTCOME ] QUOTED_STRING
Execution diagram:
Event structure diagram: