diff options
Diffstat (limited to 'language/l2.ott')
| -rw-r--r-- | language/l2.ott | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/language/l2.ott b/language/l2.ott index bf001f5c..803472a8 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -184,11 +184,14 @@ base_effect :: 'BE_' ::= | rreg :: :: rreg {{ com read register }} | wreg :: :: wreg {{ com write register }} | rmem :: :: rmem {{ com read memory }} + | rmemt :: :: rmemt {{ com read memory and tag }} | wmem :: :: wmem {{ com write memory }} - | wmea :: :: eamem {{ com signal effective address for writing memory }} - | wmv :: :: wmv {{ com write memory, sending only value }} + | wmea :: :: eamem {{ com signal effective address for writing memory }} + | exmem :: :: exmem {{ com determine if a store-exclusive (ARM) is going to succeed }} + | wmv :: :: wmv {{ com write memory, sending only value }} + | wmvt :: :: wmvt {{ com write memory, sending only value and tag }} | barr :: :: barr {{ com memory barrier }} - | depend :: :: depend {{ com dynamic footprint }} + | depend :: :: depend {{ com dynamic footprint }} | undef :: :: undef {{ com undefined-instruction exception }} | unspec :: :: unspec {{ com unspecified values }} | nondet :: :: nondet {{ com nondeterminism, from $[[nondet]]$ }} |