diff options
| author | Catalin Marinas <catalin.marinas@arm.com> | 2021-09-10 10:48:16 +0100 |
|---|---|---|
| committer | Catalin Marinas <catalin.marinas@arm.com> | 2021-09-10 10:48:16 +0100 |
| commit | 5f139826c76eff88d48fd9b4a4155ba47338af5f (patch) | |
| tree | f3d78451c7f8f98992b727376bd081cdcf0c8983 | |
| parent | 50c387fdce005e2496517bca6684248e5bb7a9b7 (diff) | |
| download | kernel-tla-5f139826c76eff88d48fd9b4a4155ba47338af5f.tar.gz | |
A previous commit inadvertently removed the implication line in the
UniqueASIDActiveTask invariant. Add it back.
Fixes: 50c387fdce00 ("asidalloc: Model PTEs and an asynchronous try_to_unmap_one() call")
Reported-by: Shameerali Kolothum Thodi <shameerali.kolothum.thodi@huawei.com>
Signed-off-by: Catalin Marinas <catalin.marinas@arm.com>
| -rw-r--r-- | asidalloc.tla | 36 |
1 files changed, 19 insertions, 17 deletions
diff --git a/asidalloc.tla b/asidalloc.tla index 25a5c7b..44ebbeb 100644 --- a/asidalloc.tla +++ b/asidalloc.tla @@ -112,6 +112,7 @@ define { /\ ActiveTask(c1) # 0 /\ ActiveTask(c2) # 0 /\ ActiveTask(c1) # ActiveTask(c2) + => ActiveAsid(c1) # ActiveAsid(c2) \* TLB empty for an active task/ASID following TLBI TLBEmptyTask(task) == \A t \in tlb : ~(t.task = task /\ t.asid = mm_context_id[task].asid) @@ -351,22 +352,22 @@ sched_loop: } } } *) -\* BEGIN TRANSLATION - the hash of the PCal code: PCal-3b4c8093cab80710385baf7e614083a3 -\* Label flush_context of procedure flush_context at line 181 col 9 changed to flush_context_ -\* Label check_update_reserved_asid of procedure check_update_reserved_asid at line 205 col 9 changed to check_update_reserved_asid_ -\* Label new_context of procedure new_context at line 223 col 9 changed to new_context_ -\* Label check_and_switch_context of procedure check_and_switch_context at line 275 col 9 changed to check_and_switch_context_ -\* Label tlb_flush_pending of procedure check_and_switch_context at line 300 col 9 changed to tlb_flush_pending_ -\* Label ttu of process ttu at line 337 col 9 changed to ttu_ -\* Procedure variable asid of procedure flush_context at line 178 col 19 changed to asid_ -\* Procedure variable cpu of procedure flush_context at line 178 col 25 changed to cpu_ -\* Procedure variable cpus of procedure flush_context at line 178 col 30 changed to cpus_ -\* Procedure variable asid of procedure new_context at line 220 col 19 changed to asid_n -\* Procedure variable newasid of procedure new_context at line 220 col 25 changed to newasid_ -\* Procedure variable asid of procedure check_and_switch_context at line 271 col 19 changed to asid_c -\* Procedure variable asid of procedure try_to_unmap at line 319 col 19 changed to asid_t -\* Parameter task of procedure new_context at line 219 col 23 changed to task_ -\* Parameter task of procedure check_and_switch_context at line 270 col 36 changed to task_c +\* BEGIN TRANSLATION - the hash of the PCal code: PCal-f21ad0e8c89501fb06f50a5b8b5a9b1f +\* Label flush_context of procedure flush_context at line 182 col 9 changed to flush_context_ +\* Label check_update_reserved_asid of procedure check_update_reserved_asid at line 206 col 9 changed to check_update_reserved_asid_ +\* Label new_context of procedure new_context at line 224 col 9 changed to new_context_ +\* Label check_and_switch_context of procedure check_and_switch_context at line 276 col 9 changed to check_and_switch_context_ +\* Label tlb_flush_pending of procedure check_and_switch_context at line 301 col 9 changed to tlb_flush_pending_ +\* Label ttu of process ttu at line 338 col 9 changed to ttu_ +\* Procedure variable asid of procedure flush_context at line 179 col 19 changed to asid_ +\* Procedure variable cpu of procedure flush_context at line 179 col 25 changed to cpu_ +\* Procedure variable cpus of procedure flush_context at line 179 col 30 changed to cpus_ +\* Procedure variable asid of procedure new_context at line 221 col 19 changed to asid_n +\* Procedure variable newasid of procedure new_context at line 221 col 25 changed to newasid_ +\* Procedure variable asid of procedure check_and_switch_context at line 272 col 19 changed to asid_c +\* Procedure variable asid of procedure try_to_unmap at line 320 col 19 changed to asid_t +\* Parameter task of procedure new_context at line 220 col 23 changed to task_ +\* Parameter task of procedure check_and_switch_context at line 271 col 36 changed to task_c CONSTANT defaultInitValue VARIABLES tlb, pte, active_mm, cpu_asid_lock, asid_generation, asid_map, active_asids, reserved_asids, tlb_flush_pending, cur_idx, @@ -440,6 +441,7 @@ UniqueASIDActiveTask == \/ ~CnP /\ ActiveTask(c1) # 0 /\ ActiveTask(c2) # 0 /\ ActiveTask(c1) # ActiveTask(c2) + => ActiveAsid(c1) # ActiveAsid(c2) TLBEmptyTask(task) == \A t \in tlb : ~(t.task = task /\ t.asid = mm_context_id[task].asid) @@ -1178,5 +1180,5 @@ Next == ttu Spec == Init /\ [][Next]_vars -\* END TRANSLATION - the hash of the generated TLA code (remove to silence divergence warnings): TLA-683adfb7ed87d6f2f601f1d0e2b708b9 +\* END TRANSLATION - the hash of the generated TLA code (remove to silence divergence warnings): TLA-071a3790d26807e2a4906e2ce2f9bf7a ============================================================================== |