Modular Relaxed Dependencies Web Tool

This tool demonstrates modular relaxed dependencies from P1780.


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