diff options
Diffstat (limited to 'src/mm-formal.adoc')
| -rw-r--r-- | src/mm-formal.adoc | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/mm-formal.adoc b/src/mm-formal.adoc index 9f2c942..58e35ee 100644 --- a/src/mm-formal.adoc +++ b/src/mm-formal.adoc @@ -597,7 +597,7 @@ continue executing. Transitions specific to `sc` instructions: [disc] -* <<early_sc_fail, Early sc fail>>: This causes the `sc` to fail, either a spontaneous fail or becauset is not paired with a program-order-previous `lr`. +* <<early_sc_fail, Early sc fail>>: This causes the `sc` to fail, either a spontaneous fail or because it is not paired with a program-order-previous `lr`. * <<paired_sc, Paired sc>>: This transition indicates the `sc` is paired with an `lr` and might succeed. @@ -1049,10 +1049,10 @@ load is acquire-RCsc. ===== Satisfy memory load operation from memory For an instruction instance latexmath:[$i$] of a non-AMO load -instruction or an AMO instruction in the context of the <<do_amo, Saitsfy, commit and propagate operations of an AMO>> transition, +instruction or an AMO instruction in the context of the <<do_amo, Satisfy, commit and propagate operations of an AMO>> transition, any memory load operation latexmath:[$mlo$] in latexmath:[$i.\textit{mem\_loads}$] that has unsatisfied slices, can be -satisfied from memory if all the conditions of <sat_by_forwarding, Saitsfy memory load operation by forwarding from unpropagated stores>> are satisfied. Action: +satisfied from memory if all the conditions of <sat_by_forwarding, Satisfy memory load operation by forwarding from unpropagated stores>> are satisfied. Action: let latexmath:[$msoss$] be the memory store operation slices from memory covering the unsatisfied slices of latexmath:[$mlo$], and apply the action of <<do_amo, Satisfy memory operation by forwarding from unpropagates stores>>. @@ -1259,7 +1259,7 @@ Plain(_store_continuation(false)_). For efficiency, the `rmem` tool allows this transition only when it is not possible to take the <<commit_sc, Commit and propagate store operation of an sc>> transition. This does not affect the set of allowed final states, but when explored interactively, if the `sc` -should fail one should use the <<early_sc_fail, Eaarly sc fail>> transition instead of waiting for this transition. +should fail one should use the <<early_sc_fail, Early sc fail>> transition instead of waiting for this transition. ==== [[complete_stores]] ===== Complete store operations |