diff options
| author | Jon French | 2017-07-21 19:21:45 +0100 |
|---|---|---|
| committer | Jon French | 2017-07-21 20:56:56 +0100 |
| commit | 4683962ecbb42167d6d966d731c451ba5eb696d5 (patch) | |
| tree | 8550d2c0e930d119c1152f37c4c557ac77cc8609 | |
| parent | a44803592030e06bbd91572287d50bd538560fd3 (diff) | |
l2.ott: port across additions to base_effect from rmem
| -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]]$ }} |