| ------------------------------ MODULE fpsimd --------------------------------- |
| EXTENDS Naturals, Sequences, FiniteSets, TLC |
| |
| CONSTANTS CPUS, \* set of available CPUs |
| THREADS, \* set of threads |
| VALS \* set of register values |
| |
| \* Generic helpers |
| Range(func) == |
| {func[e] : e \in DOMAIN func} |
| |
| (* --algorithm fpsimd { |
| variables |
| \* OS and hardware state |
| \* Select distinct init threads for each CPU |
| cpu \in {c \in [THREADS -> CPUS \cup {"none"}] : |
| /\ Cardinality(Range(c) \ {"none"}) = Cardinality(CPUS) |
| /\ \A t1, t2 \in THREADS : |
| t1 # t2 => c[t1] = "none" \/ c[t1] # c[t2]}; |
| \* Remove the init threads from the runqueue |
| runqueue = THREADS \ {t \in THREADS : cpu[t] # "none"}; |
| interrupts = [p \in CPUS |-> "off"]; |
| in_interrupt = [t \in THREADS |-> FALSE]; |
| mode = [t \in THREADS |-> "user"]; |
| preempt_count = [t \in THREADS |-> 0]; |
| |
| \* Thread state |
| thread = [t \in THREADS |-> |
| [fpsimd_state |-> "zero", |
| fpsimd_cpu |-> "none", |
| sve_state |-> << "zero", "zero" >>, |
| flags |-> {"TIF_FOREIGN_FPSTATE"}]]; |
| |
| \* FPSIMD state tracking |
| fpsimd_last_state = [p \in CPUS |-> "null"]; |
| fpsimd_context_busy = [p \in CPUS |-> FALSE]; |
| |
| \* Hardware << FPSIMD, SVE >> vectors |
| hwfpsimd = [p \in CPUS |-> << "zero", "zero" >>]; |
| sve_user_trap = [p \in CPUS |-> TRUE]; |
| |
| define { |
| \* |
| \* Type invariants |
| \* |
| ThreadFlags == {"TIF_FOREIGN_FPSTATE", "TIF_SVE"} |
| FPSIMDType == VALS \cup {"zero"} |
| SVEType == FPSIMDType \X FPSIMDType |
| ThreadStateType == |
| [fpsimd_state: FPSIMDType, |
| fpsimd_cpu: CPUS \cup {"none"}, |
| sve_state: SVEType, |
| flags: SUBSET ThreadFlags] |
| TypeInv == |
| /\ thread \in [THREADS -> ThreadStateType] |
| /\ runqueue \subseteq THREADS |
| /\ interrupts \in [CPUS -> {"on", "off"}] |
| /\ in_interrupt \in [THREADS -> BOOLEAN] |
| /\ cpu \in [THREADS -> CPUS \cup {"none"}] |
| /\ preempt_count \in [THREADS -> Nat] |
| /\ mode \in [THREADS -> {"user", "kernel"}] |
| /\ hwfpsimd \in [CPUS -> SVEType] |
| /\ sve_user_trap \in [CPUS -> BOOLEAN] |
| /\ fpsimd_last_state \in [CPUS -> THREADS \cup {"null"}] |
| /\ fpsimd_context_busy \in [CPUS -> BOOLEAN] |
| |
| \* |
| \* Scheduler invariants |
| \* |
| SchedInv == |
| /\ Cardinality(Range(cpu) \ {"none"}) = Cardinality(CPUS) |
| /\ \A t1, t2 \in THREADS : |
| t1 # t2 => cpu[t1] = "none" \/ cpu[t1] # cpu[t2] |
| /\ \A t \in runqueue : cpu[t] = "none" |
| |
| \* Symmetry optimisations |
| Perms == Permutations(CPUS) \cup Permutations(THREADS) \cup |
| Permutations(VALS) |
| } |
| |
| \* Interrupts enabling/disabling |
| macro interrupts_enable() { |
| interrupts[cpu[self]] := "on"; |
| } |
| |
| macro interrupts_disable() { |
| interrupts[cpu[self]] := "off"; |
| } |
| |
| macro preempt_disable() { |
| preempt_count[self] := preempt_count[self] + 1; |
| } |
| |
| macro preempt_enable() { |
| preempt_count[self] := preempt_count[self] - 1; |
| } |
| |
| \* Thread flag manipulation |
| macro set_thread_flag(thr, flag) { |
| thread[thr].flags := thread[thr].flags \cup {flag}; |
| } |
| |
| macro clear_thread_flag(thr, flag) { |
| thread[thr].flags := thread[thr].flags \ {flag}; |
| } |
| |
| \* FPSIMD/SVE register reading/writing with the expected value |
| \* stored in the local variable "val" |
| macro write_fpsimd(v, val) { |
| val := << v, "zero" >>; |
| hwfpsimd[cpu[self]] := val; |
| } |
| |
| macro read_fpsimd(val) { |
| assert hwfpsimd[cpu[self]][1] = val[1]; |
| } |
| |
| macro write_sve(vv, val) { |
| val := vv; |
| hwfpsimd[cpu[self]] := val; |
| } |
| |
| macro read_sve(val) { |
| assert hwfpsimd[cpu[self]] = val; |
| } |
| |
| \* Update current thread for the CPU |
| macro cpu_switch_to(next) |
| { |
| cpu[next] := cpu[self] || |
| cpu[self] := "none"; |
| } |
| |
| macro sleep() |
| { |
| await cpu[self] # "none"; |
| } |
| |
| macro __get_cpu_fpsimd_context() |
| { |
| assert ~fpsimd_context_busy[cpu[self]]; |
| fpsimd_context_busy[cpu[self]] := TRUE; |
| } |
| |
| macro __put_cpu_fpsimd_context() |
| { |
| assert fpsimd_context_busy[cpu[self]]; |
| fpsimd_context_busy[cpu[self]] := FALSE; |
| } |
| |
| macro get_cpu_fpsimd_context() |
| { |
| preempt_disable(); |
| __get_cpu_fpsimd_context(); |
| } |
| |
| macro put_cpu_fpsimd_context() |
| { |
| __put_cpu_fpsimd_context(); |
| preempt_enable(); |
| } |
| |
| macro fpsimd_save_state() { |
| thread[self].fpsimd_state := hwfpsimd[cpu[self]][1]; |
| } |
| |
| macro fpsimd_load_state() { |
| hwfpsimd[cpu[self]] := << thread[self].fpsimd_state, "zero" >>; |
| } |
| |
| macro sve_save_state() { |
| thread[self].sve_state := hwfpsimd[cpu[self]]; |
| } |
| |
| macro sve_load_state() { |
| hwfpsimd[cpu[self]] := thread[self].sve_state; |
| } |
| |
| macro sve_user_enable() { |
| sve_user_trap[cpu[self]] := FALSE; |
| } |
| |
| macro sve_user_disable() { |
| sve_user_trap[cpu[self]] := TRUE; |
| } |
| |
| macro fpsimd_save() { |
| assert fpsimd_context_busy[cpu[self]]; |
| if ("TIF_FOREIGN_FPSTATE" \notin thread[self].flags) { |
| if ("TIF_SVE" \in thread[self].flags) |
| sve_save_state(); |
| else |
| fpsimd_save_state(); |
| } |
| } |
| |
| macro task_fpsimd_load() { |
| assert fpsimd_context_busy[cpu[self]]; |
| if ("TIF_SVE" \in thread[self].flags) |
| sve_load_state(); |
| else |
| fpsimd_load_state(); |
| } |
| |
| macro fpsimd_to_sve() { |
| thread[self].sve_state := << thread[self].fpsimd_state, "zero" >>; |
| } |
| |
| macro fpsimd_bind_task_to_cpu() { |
| fpsimd_last_state[cpu[self]] := self; |
| thread[self].fpsimd_cpu := cpu[self]; |
| if ("TIF_SVE" \in thread[self].flags) |
| sve_user_enable(); |
| else |
| sve_user_disable(); |
| } |
| |
| macro fpsimd_flush_task_state() { |
| \* set_thread_flag() does not work with the || operator |
| thread[self].fpsimd_cpu := "none" || |
| thread[self].flags := thread[self].flags \cup {"TIF_FOREIGN_FPSTATE"}; |
| } |
| |
| macro fpsimd_flush_cpu_state() { |
| fpsimd_last_state[cpu[self]] := "null"; |
| set_thread_flag(self, "TIF_FOREIGN_FPSTATE"); |
| } |
| |
| macro sve_user_discard() { |
| clear_thread_flag(self, "TIF_SVE"); |
| sve_user_disable(); |
| } |
| |
| procedure kernel_neon_begin() |
| { |
| knb1: get_cpu_fpsimd_context(); |
| knb2: fpsimd_save(); |
| knb3: fpsimd_flush_cpu_state(); |
| return; |
| } |
| |
| procedure kernel_neon_end() |
| { |
| kne1: put_cpu_fpsimd_context(); |
| return; |
| } |
| |
| procedure fpsimd_restore_current_state() |
| { |
| frcs1: get_cpu_fpsimd_context(); |
| frcs2: if ("TIF_FOREIGN_FPSTATE" \in thread[self].flags) { |
| clear_thread_flag(self, "TIF_FOREIGN_FPSTATE"); |
| frcs3: task_fpsimd_load(); |
| fpsimd_bind_task_to_cpu(); |
| }; |
| frcs4: put_cpu_fpsimd_context(); |
| return; |
| } |
| |
| \* FPSIMD/SVE state switching |
| procedure fpsimd_thread_switch(next) |
| { |
| fts1: __get_cpu_fpsimd_context(); |
| fpsimd_save(); |
| fts2: \* wrong_task or wrong_cpu |
| if (fpsimd_last_state[cpu[self]] # next \/ |
| thread[next].fpsimd_cpu # cpu[self]) |
| set_thread_flag(next, "TIF_FOREIGN_FPSTATE"); |
| else |
| clear_thread_flag(next, "TIF_FOREIGN_FPSTATE"); |
| fts3: __put_cpu_fpsimd_context(); |
| return; |
| } |
| |
| procedure schedule() |
| variables next; |
| { |
| sch1: assert preempt_count[self] = 0; |
| assert interrupts[cpu[self]] = "off"; |
| with (n \in runqueue \cup {"none"}) { |
| if (n = "none") { |
| \* Return if no new thread to schedule |
| interrupts_enable(); |
| return; |
| } else { |
| \* Remove the next thread from the runqueue and schedule |
| runqueue := runqueue \ {n}; |
| next := n; |
| }; |
| }; |
| sch2: call fpsimd_thread_switch(next); |
| sch3: \* Add the previous thread to the runqueue and switch to next |
| runqueue := runqueue \cup {self}; |
| cpu_switch_to(next); |
| sch4: \* Context switching done, wait to be rescheduled |
| sleep(); |
| sch5: interrupts_enable(); |
| return; |
| } |
| |
| procedure do_notify_resume() |
| { |
| dnr1: assert interrupts[cpu[self]] = "off"; |
| call schedule(); |
| dnr2: if ("TIF_FOREIGN_FPSTATE" \in thread[self].flags) |
| call fpsimd_restore_current_state(); |
| dnr3: interrupts_disable(); |
| \* repeat if more work needed |
| if ("TIF_FOREIGN_FPSTATE" \in thread[self].flags) |
| goto dnr1; |
| else |
| return; |
| } |
| |
| \* Interrupt handler |
| procedure interrupt_handler() |
| { |
| handle_int: |
| interrupts_disable(); |
| in_interrupt[self] := TRUE; |
| if (mode[self] = "user") |
| call do_notify_resume(); |
| else if (preempt_count[self] = 0) |
| call schedule(); |
| int1: in_interrupt[self] := FALSE; |
| interrupts_enable(); |
| return; |
| } |
| |
| procedure do_sve_acc() |
| { |
| dsa1: mode[self] := "kernel"; |
| |
| dsa2: get_cpu_fpsimd_context(); |
| fpsimd_save(); |
| dsa3: fpsimd_flush_task_state(); |
| dsa4: fpsimd_to_sve(); |
| dsa5: set_thread_flag(self, "TIF_SVE"); |
| put_cpu_fpsimd_context(); |
| |
| \* ret_to_user |
| dsa6: interrupts_disable(); |
| call do_notify_resume(); |
| dsa7: mode[self] := "user"; |
| interrupts_enable(); |
| return; |
| } |
| |
| procedure kernel_neon() |
| variable kval; |
| { |
| kn1: call kernel_neon_begin(); |
| kn2: with (v \in VALS) write_fpsimd(v, kval); |
| kn3: read_fpsimd(kval); |
| call kernel_neon_end(); |
| return; |
| } |
| |
| procedure syscall() |
| { |
| sys_entry: |
| mode[self] := "kernel"; |
| sve_user_discard(); |
| \* exercise in-kernel FPSIMD |
| sys1: while (TRUE) { |
| either call kernel_neon(); |
| or goto ret_to_user; |
| }; |
| ret_to_user: |
| interrupts_disable(); |
| call do_notify_resume(); |
| sys2: mode[self] := "user"; |
| interrupts_enable(); |
| return; |
| } |
| |
| \* User threads |
| process (thread \in THREADS) |
| variable val = << "zero", "zero" >>; |
| { |
| thr1: \* wait to be scheduled (simulate thread creation) |
| sleep(); |
| \* FPSIMD initialisation (normally done by do_notify_resume()) |
| call fpsimd_restore_current_state(); |
| thr2: interrupts_enable(); |
| thr3: \* user thread actions |
| while (TRUE) { |
| \* FPSIMD read/write |
| either { with (v \in VALS) write_fpsimd(v, val); } |
| or { read_fpsimd(val); } |
| \* SVE read/write/trap |
| or { when ~sve_user_trap[cpu[self]]; with (v \in VALS \X VALS) write_sve(v, val); } |
| or { when ~sve_user_trap[cpu[self]]; read_sve(val); } |
| or { when sve_user_trap[cpu[self]]; call do_sve_acc(); } |
| \* syscall; discard the SVE state |
| or { val[2] := "zero"; call syscall(); } |
| } |
| } |
| } *) |
| ------------------------------------------------------------------------------ |
| \* BEGIN TRANSLATION |
| \* Process thread at line 378 col 1 changed to thread_ |
| \* Procedure variable next of procedure schedule at line 276 col 19 changed to next_ |
| CONSTANT defaultInitValue |
| VARIABLES cpu, runqueue, interrupts, in_interrupt, mode, preempt_count, |
| thread, fpsimd_last_state, fpsimd_context_busy, hwfpsimd, |
| sve_user_trap, pc, stack |
| |
| (* define statement *) |
| ThreadFlags == {"TIF_FOREIGN_FPSTATE", "TIF_SVE"} |
| FPSIMDType == VALS \cup {"zero"} |
| SVEType == FPSIMDType \X FPSIMDType |
| ThreadStateType == |
| [fpsimd_state: FPSIMDType, |
| fpsimd_cpu: CPUS \cup {"none"}, |
| sve_state: SVEType, |
| flags: SUBSET ThreadFlags] |
| TypeInv == |
| /\ thread \in [THREADS -> ThreadStateType] |
| /\ runqueue \subseteq THREADS |
| /\ interrupts \in [CPUS -> {"on", "off"}] |
| /\ in_interrupt \in [THREADS -> BOOLEAN] |
| /\ cpu \in [THREADS -> CPUS \cup {"none"}] |
| /\ preempt_count \in [THREADS -> Nat] |
| /\ mode \in [THREADS -> {"user", "kernel"}] |
| /\ hwfpsimd \in [CPUS -> SVEType] |
| /\ sve_user_trap \in [CPUS -> BOOLEAN] |
| /\ fpsimd_last_state \in [CPUS -> THREADS \cup {"null"}] |
| /\ fpsimd_context_busy \in [CPUS -> BOOLEAN] |
| |
| |
| |
| |
| SchedInv == |
| /\ Cardinality(Range(cpu) \ {"none"}) = Cardinality(CPUS) |
| /\ \A t1, t2 \in THREADS : |
| t1 # t2 => cpu[t1] = "none" \/ cpu[t1] # cpu[t2] |
| /\ \A t \in runqueue : cpu[t] = "none" |
| |
| |
| Perms == Permutations(CPUS) \cup Permutations(THREADS) \cup |
| Permutations(VALS) |
| |
| VARIABLES next, next_, kval, val |
| |
| global_vars == << sve_user_trap, hwfpsimd, mode, fpsimd_last_state, preempt_count, fpsimd_context_busy, thread, cpu, in_interrupt, interrupts, runqueue >> |
| local_vars == << next, val, next_, kval >> |
| vars == << global_vars, local_vars, pc, stack >> |
| |
| ProcSet == (THREADS) |
| |
| Init == (* Global variables *) |
| /\ cpu \in {c \in [THREADS -> CPUS \cup {"none"}] : |
| /\ Cardinality(Range(c) \ {"none"}) = Cardinality(CPUS) |
| /\ \A t1, t2 \in THREADS : |
| t1 # t2 => c[t1] = "none" \/ c[t1] # c[t2]} |
| /\ runqueue = THREADS \ {t \in THREADS : cpu[t] # "none"} |
| /\ interrupts = [p \in CPUS |-> "off"] |
| /\ in_interrupt = [t \in THREADS |-> FALSE] |
| /\ mode = [t \in THREADS |-> "user"] |
| /\ preempt_count = [t \in THREADS |-> 0] |
| /\ thread = [t \in THREADS |-> |
| [fpsimd_state |-> "zero", |
| fpsimd_cpu |-> "none", |
| sve_state |-> << "zero", "zero" >>, |
| flags |-> {"TIF_FOREIGN_FPSTATE"}]] |
| /\ fpsimd_last_state = [p \in CPUS |-> "null"] |
| /\ fpsimd_context_busy = [p \in CPUS |-> FALSE] |
| /\ hwfpsimd = [p \in CPUS |-> << "zero", "zero" >>] |
| /\ sve_user_trap = [p \in CPUS |-> TRUE] |
| (* Procedure fpsimd_thread_switch *) |
| /\ next = [ self \in ProcSet |-> defaultInitValue] |
| (* Procedure schedule *) |
| /\ next_ = [ self \in ProcSet |-> defaultInitValue] |
| (* Procedure kernel_neon *) |
| /\ kval = [ self \in ProcSet |-> defaultInitValue] |
| (* Process thread_ *) |
| /\ val = [self \in THREADS |-> << "zero", "zero" >>] |
| /\ stack = [self \in ProcSet |-> << >>] |
| /\ pc = [self \in ProcSet |-> "thr1"] |
| |
| knb1(self) == /\ pc[self] = "knb1" |
| /\ preempt_count' = [preempt_count EXCEPT ![self] = preempt_count[self] + 1] |
| /\ Assert(~fpsimd_context_busy[cpu[self]], |
| "Failure of assertion at line 141, column 9 of macro called at line 236, column 9.") |
| /\ fpsimd_context_busy' = [fpsimd_context_busy EXCEPT ![cpu[self]] = TRUE] |
| /\ pc' = [pc EXCEPT ![self] = "knb2"] |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, |
| thread, fpsimd_last_state, hwfpsimd, |
| sve_user_trap, stack, next, next_, kval, val >> |
| |
| knb2(self) == /\ pc[self] = "knb2" |
| /\ Assert(fpsimd_context_busy[cpu[self]], |
| "Failure of assertion at line 188, column 9 of macro called at line 237, column 9.") |
| /\ IF "TIF_FOREIGN_FPSTATE" \notin thread[self].flags |
| THEN /\ IF "TIF_SVE" \in thread[self].flags |
| THEN /\ thread' = [thread EXCEPT ![self].sve_state = hwfpsimd[cpu[self]]] |
| ELSE /\ thread' = [thread EXCEPT ![self].fpsimd_state = hwfpsimd[cpu[self]][1]] |
| ELSE /\ TRUE |
| /\ UNCHANGED thread |
| /\ pc' = [pc EXCEPT ![self] = "knb3"] |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, |
| preempt_count, fpsimd_last_state, |
| fpsimd_context_busy, hwfpsimd, sve_user_trap, |
| stack, next, next_, kval, val >> |
| |
| knb3(self) == /\ pc[self] = "knb3" |
| /\ fpsimd_last_state' = [fpsimd_last_state EXCEPT ![cpu[self]] = "null"] |
| /\ thread' = [thread EXCEPT ![self].flags = thread[self].flags \cup {"TIF_FOREIGN_FPSTATE"}] |
| /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] |
| /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, |
| preempt_count, fpsimd_context_busy, hwfpsimd, |
| sve_user_trap, next, next_, kval, val >> |
| |
| kernel_neon_begin(self) == knb1(self) \/ knb2(self) \/ knb3(self) |
| |
| kne1(self) == /\ pc[self] = "kne1" |
| /\ Assert(fpsimd_context_busy[cpu[self]], |
| "Failure of assertion at line 147, column 9 of macro called at line 244, column 9.") |
| /\ fpsimd_context_busy' = [fpsimd_context_busy EXCEPT ![cpu[self]] = FALSE] |
| /\ preempt_count' = [preempt_count EXCEPT ![self] = preempt_count[self] - 1] |
| /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] |
| /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, |
| thread, fpsimd_last_state, hwfpsimd, |
| sve_user_trap, next, next_, kval, val >> |
| |
| kernel_neon_end(self) == kne1(self) |
| |
| frcs1(self) == /\ pc[self] = "frcs1" |
| /\ preempt_count' = [preempt_count EXCEPT ![self] = preempt_count[self] + 1] |
| /\ Assert(~fpsimd_context_busy[cpu[self]], |
| "Failure of assertion at line 141, column 9 of macro called at line 250, column 9.") |
| /\ fpsimd_context_busy' = [fpsimd_context_busy EXCEPT ![cpu[self]] = TRUE] |
| /\ pc' = [pc EXCEPT ![self] = "frcs2"] |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, |
| thread, fpsimd_last_state, hwfpsimd, |
| sve_user_trap, stack, next, next_, kval, val >> |
| |
| frcs2(self) == /\ pc[self] = "frcs2" |
| /\ IF "TIF_FOREIGN_FPSTATE" \in thread[self].flags |
| THEN /\ thread' = [thread EXCEPT ![self].flags = thread[self].flags \ {"TIF_FOREIGN_FPSTATE"}] |
| /\ pc' = [pc EXCEPT ![self] = "frcs3"] |
| ELSE /\ pc' = [pc EXCEPT ![self] = "frcs4"] |
| /\ UNCHANGED thread |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, |
| preempt_count, fpsimd_last_state, |
| fpsimd_context_busy, hwfpsimd, sve_user_trap, |
| stack, next, next_, kval, val >> |
| |
| frcs3(self) == /\ pc[self] = "frcs3" |
| /\ Assert(fpsimd_context_busy[cpu[self]], |
| "Failure of assertion at line 198, column 9 of macro called at line 253, column 17.") |
| /\ IF "TIF_SVE" \in thread[self].flags |
| THEN /\ hwfpsimd' = [hwfpsimd EXCEPT ![cpu[self]] = thread[self].sve_state] |
| ELSE /\ hwfpsimd' = [hwfpsimd EXCEPT ![cpu[self]] = << thread[self].fpsimd_state, "zero" >>] |
| /\ fpsimd_last_state' = [fpsimd_last_state EXCEPT ![cpu[self]] = self] |
| /\ thread' = [thread EXCEPT ![self].fpsimd_cpu = cpu[self]] |
| /\ IF "TIF_SVE" \in thread'[self].flags |
| THEN /\ sve_user_trap' = [sve_user_trap EXCEPT ![cpu[self]] = FALSE] |
| ELSE /\ sve_user_trap' = [sve_user_trap EXCEPT ![cpu[self]] = TRUE] |
| /\ pc' = [pc EXCEPT ![self] = "frcs4"] |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, |
| preempt_count, fpsimd_context_busy, stack, next, |
| next_, kval, val >> |
| |
| frcs4(self) == /\ pc[self] = "frcs4" |
| /\ Assert(fpsimd_context_busy[cpu[self]], |
| "Failure of assertion at line 147, column 9 of macro called at line 256, column 9.") |
| /\ fpsimd_context_busy' = [fpsimd_context_busy EXCEPT ![cpu[self]] = FALSE] |
| /\ preempt_count' = [preempt_count EXCEPT ![self] = preempt_count[self] - 1] |
| /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] |
| /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, |
| thread, fpsimd_last_state, hwfpsimd, |
| sve_user_trap, next, next_, kval, val >> |
| |
| fpsimd_restore_current_state(self) == frcs1(self) \/ frcs2(self) |
| \/ frcs3(self) \/ frcs4(self) |
| |
| fts1(self) == /\ pc[self] = "fts1" |
| /\ Assert(~fpsimd_context_busy[cpu[self]], |
| "Failure of assertion at line 141, column 9 of macro called at line 263, column 9.") |
| /\ fpsimd_context_busy' = [fpsimd_context_busy EXCEPT ![cpu[self]] = TRUE] |
| /\ Assert(fpsimd_context_busy'[cpu[self]], |
| "Failure of assertion at line 188, column 9 of macro called at line 264, column 9.") |
| /\ IF "TIF_FOREIGN_FPSTATE" \notin thread[self].flags |
| THEN /\ IF "TIF_SVE" \in thread[self].flags |
| THEN /\ thread' = [thread EXCEPT ![self].sve_state = hwfpsimd[cpu[self]]] |
| ELSE /\ thread' = [thread EXCEPT ![self].fpsimd_state = hwfpsimd[cpu[self]][1]] |
| ELSE /\ TRUE |
| /\ UNCHANGED thread |
| /\ pc' = [pc EXCEPT ![self] = "fts2"] |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, |
| preempt_count, fpsimd_last_state, hwfpsimd, |
| sve_user_trap, stack, next, next_, kval, val >> |
| |
| fts2(self) == /\ pc[self] = "fts2" |
| /\ IF fpsimd_last_state[cpu[self]] # next[self] \/ |
| thread[next[self]].fpsimd_cpu # cpu[self] |
| THEN /\ thread' = [thread EXCEPT ![next[self]].flags = thread[next[self]].flags \cup {"TIF_FOREIGN_FPSTATE"}] |
| ELSE /\ thread' = [thread EXCEPT ![next[self]].flags = thread[next[self]].flags \ {"TIF_FOREIGN_FPSTATE"}] |
| /\ pc' = [pc EXCEPT ![self] = "fts3"] |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, |
| preempt_count, fpsimd_last_state, |
| fpsimd_context_busy, hwfpsimd, sve_user_trap, |
| stack, next, next_, kval, val >> |
| |
| fts3(self) == /\ pc[self] = "fts3" |
| /\ Assert(fpsimd_context_busy[cpu[self]], |
| "Failure of assertion at line 147, column 9 of macro called at line 271, column 9.") |
| /\ fpsimd_context_busy' = [fpsimd_context_busy EXCEPT ![cpu[self]] = FALSE] |
| /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] |
| /\ next' = [next EXCEPT ![self] = Head(stack[self]).next] |
| /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, |
| preempt_count, thread, fpsimd_last_state, |
| hwfpsimd, sve_user_trap, next_, kval, val >> |
| |
| fpsimd_thread_switch(self) == fts1(self) \/ fts2(self) \/ fts3(self) |
| |
| sch1(self) == /\ pc[self] = "sch1" |
| /\ Assert(preempt_count[self] = 0, |
| "Failure of assertion at line 278, column 9.") |
| /\ Assert(interrupts[cpu[self]] = "off", |
| "Failure of assertion at line 279, column 9.") |
| /\ \E n \in runqueue \cup {"none"}: |
| IF n = "none" |
| THEN /\ interrupts' = [interrupts EXCEPT ![cpu[self]] = "on"] |
| /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] |
| /\ next_' = [next_ EXCEPT ![self] = Head(stack[self]).next_] |
| /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] |
| /\ UNCHANGED runqueue |
| ELSE /\ runqueue' = runqueue \ {n} |
| /\ next_' = [next_ EXCEPT ![self] = n] |
| /\ pc' = [pc EXCEPT ![self] = "sch2"] |
| /\ UNCHANGED << interrupts, stack >> |
| /\ UNCHANGED << cpu, in_interrupt, mode, preempt_count, thread, |
| fpsimd_last_state, fpsimd_context_busy, hwfpsimd, |
| sve_user_trap, next, kval, val >> |
| |
| sch2(self) == /\ pc[self] = "sch2" |
| /\ /\ next' = [next EXCEPT ![self] = next_[self]] |
| /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "fpsimd_thread_switch", |
| pc |-> "sch3", |
| next |-> next[self] ] >> |
| \o stack[self]] |
| /\ pc' = [pc EXCEPT ![self] = "fts1"] |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, |
| preempt_count, thread, fpsimd_last_state, |
| fpsimd_context_busy, hwfpsimd, sve_user_trap, |
| next_, kval, val >> |
| |
| sch3(self) == /\ pc[self] = "sch3" |
| /\ runqueue' = (runqueue \cup {self}) |
| /\ cpu' = [cpu EXCEPT ![next_[self]] = cpu[self], |
| ![self] = "none"] |
| /\ pc' = [pc EXCEPT ![self] = "sch4"] |
| /\ UNCHANGED << interrupts, in_interrupt, mode, preempt_count, |
| thread, fpsimd_last_state, fpsimd_context_busy, |
| hwfpsimd, sve_user_trap, stack, next, next_, |
| kval, val >> |
| |
| sch4(self) == /\ pc[self] = "sch4" |
| /\ cpu[self] # "none" |
| /\ pc' = [pc EXCEPT ![self] = "sch5"] |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, |
| preempt_count, thread, fpsimd_last_state, |
| fpsimd_context_busy, hwfpsimd, sve_user_trap, |
| stack, next, next_, kval, val >> |
| |
| sch5(self) == /\ pc[self] = "sch5" |
| /\ interrupts' = [interrupts EXCEPT ![cpu[self]] = "on"] |
| /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] |
| /\ next_' = [next_ EXCEPT ![self] = Head(stack[self]).next_] |
| /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] |
| /\ UNCHANGED << cpu, runqueue, in_interrupt, mode, preempt_count, |
| thread, fpsimd_last_state, fpsimd_context_busy, |
| hwfpsimd, sve_user_trap, next, kval, val >> |
| |
| schedule(self) == sch1(self) \/ sch2(self) \/ sch3(self) \/ sch4(self) |
| \/ sch5(self) |
| |
| dnr1(self) == /\ pc[self] = "dnr1" |
| /\ Assert(interrupts[cpu[self]] = "off", |
| "Failure of assertion at line 303, column 9.") |
| /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "schedule", |
| pc |-> "dnr2", |
| next_ |-> next_[self] ] >> |
| \o stack[self]] |
| /\ next_' = [next_ EXCEPT ![self] = defaultInitValue] |
| /\ pc' = [pc EXCEPT ![self] = "sch1"] |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, |
| preempt_count, thread, fpsimd_last_state, |
| fpsimd_context_busy, hwfpsimd, sve_user_trap, |
| next, kval, val >> |
| |
| dnr2(self) == /\ pc[self] = "dnr2" |
| /\ IF "TIF_FOREIGN_FPSTATE" \in thread[self].flags |
| THEN /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "fpsimd_restore_current_state", |
| pc |-> "dnr3" ] >> |
| \o stack[self]] |
| /\ pc' = [pc EXCEPT ![self] = "frcs1"] |
| ELSE /\ pc' = [pc EXCEPT ![self] = "dnr3"] |
| /\ stack' = stack |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, |
| preempt_count, thread, fpsimd_last_state, |
| fpsimd_context_busy, hwfpsimd, sve_user_trap, |
| next, next_, kval, val >> |
| |
| dnr3(self) == /\ pc[self] = "dnr3" |
| /\ interrupts' = [interrupts EXCEPT ![cpu[self]] = "off"] |
| /\ IF "TIF_FOREIGN_FPSTATE" \in thread[self].flags |
| THEN /\ pc' = [pc EXCEPT ![self] = "dnr1"] |
| /\ stack' = stack |
| ELSE /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] |
| /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] |
| /\ UNCHANGED << cpu, runqueue, in_interrupt, mode, preempt_count, |
| thread, fpsimd_last_state, fpsimd_context_busy, |
| hwfpsimd, sve_user_trap, next, next_, kval, val >> |
| |
| do_notify_resume(self) == dnr1(self) \/ dnr2(self) \/ dnr3(self) |
| |
| handle_int(self) == /\ pc[self] = "handle_int" |
| /\ interrupts' = [interrupts EXCEPT ![cpu[self]] = "off"] |
| /\ in_interrupt' = [in_interrupt EXCEPT ![self] = TRUE] |
| /\ IF mode[self] = "user" |
| THEN /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "do_notify_resume", |
| pc |-> "int1" ] >> |
| \o stack[self]] |
| /\ pc' = [pc EXCEPT ![self] = "dnr1"] |
| /\ next_' = next_ |
| ELSE /\ IF preempt_count[self] = 0 |
| THEN /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "schedule", |
| pc |-> "int1", |
| next_ |-> next_[self] ] >> |
| \o stack[self]] |
| /\ next_' = [next_ EXCEPT ![self] = defaultInitValue] |
| /\ pc' = [pc EXCEPT ![self] = "sch1"] |
| ELSE /\ pc' = [pc EXCEPT ![self] = "int1"] |
| /\ UNCHANGED << stack, next_ >> |
| /\ UNCHANGED << cpu, runqueue, mode, preempt_count, thread, |
| fpsimd_last_state, fpsimd_context_busy, |
| hwfpsimd, sve_user_trap, next, kval, val >> |
| |
| int1(self) == /\ pc[self] = "int1" |
| /\ in_interrupt' = [in_interrupt EXCEPT ![self] = FALSE] |
| /\ interrupts' = [interrupts EXCEPT ![cpu[self]] = "on"] |
| /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] |
| /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] |
| /\ UNCHANGED << cpu, runqueue, mode, preempt_count, thread, |
| fpsimd_last_state, fpsimd_context_busy, hwfpsimd, |
| sve_user_trap, next, next_, kval, val >> |
| |
| interrupt_handler(self) == handle_int(self) \/ int1(self) |
| |
| dsa1(self) == /\ pc[self] = "dsa1" |
| /\ mode' = [mode EXCEPT ![self] = "kernel"] |
| /\ pc' = [pc EXCEPT ![self] = "dsa2"] |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, |
| preempt_count, thread, fpsimd_last_state, |
| fpsimd_context_busy, hwfpsimd, sve_user_trap, |
| stack, next, next_, kval, val >> |
| |
| dsa2(self) == /\ pc[self] = "dsa2" |
| /\ preempt_count' = [preempt_count EXCEPT ![self] = preempt_count[self] + 1] |
| /\ Assert(~fpsimd_context_busy[cpu[self]], |
| "Failure of assertion at line 141, column 9 of macro called at line 334, column 9.") |
| /\ fpsimd_context_busy' = [fpsimd_context_busy EXCEPT ![cpu[self]] = TRUE] |
| /\ Assert(fpsimd_context_busy'[cpu[self]], |
| "Failure of assertion at line 188, column 9 of macro called at line 335, column 9.") |
| /\ IF "TIF_FOREIGN_FPSTATE" \notin thread[self].flags |
| THEN /\ IF "TIF_SVE" \in thread[self].flags |
| THEN /\ thread' = [thread EXCEPT ![self].sve_state = hwfpsimd[cpu[self]]] |
| ELSE /\ thread' = [thread EXCEPT ![self].fpsimd_state = hwfpsimd[cpu[self]][1]] |
| ELSE /\ TRUE |
| /\ UNCHANGED thread |
| /\ pc' = [pc EXCEPT ![self] = "dsa3"] |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, |
| fpsimd_last_state, hwfpsimd, sve_user_trap, |
| stack, next, next_, kval, val >> |
| |
| dsa3(self) == /\ pc[self] = "dsa3" |
| /\ thread' = [thread EXCEPT ![self].fpsimd_cpu = "none", |
| ![self].flags = thread[self].flags \cup {"TIF_FOREIGN_FPSTATE"}] |
| /\ pc' = [pc EXCEPT ![self] = "dsa4"] |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, |
| preempt_count, fpsimd_last_state, |
| fpsimd_context_busy, hwfpsimd, sve_user_trap, |
| stack, next, next_, kval, val >> |
| |
| dsa4(self) == /\ pc[self] = "dsa4" |
| /\ thread' = [thread EXCEPT ![self].sve_state = << thread[self].fpsimd_state, "zero" >>] |
| /\ pc' = [pc EXCEPT ![self] = "dsa5"] |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, |
| preempt_count, fpsimd_last_state, |
| fpsimd_context_busy, hwfpsimd, sve_user_trap, |
| stack, next, next_, kval, val >> |
| |
| dsa5(self) == /\ pc[self] = "dsa5" |
| /\ thread' = [thread EXCEPT ![self].flags = thread[self].flags \cup {"TIF_SVE"}] |
| /\ Assert(fpsimd_context_busy[cpu[self]], |
| "Failure of assertion at line 147, column 9 of macro called at line 339, column 9.") |
| /\ fpsimd_context_busy' = [fpsimd_context_busy EXCEPT ![cpu[self]] = FALSE] |
| /\ preempt_count' = [preempt_count EXCEPT ![self] = preempt_count[self] - 1] |
| /\ pc' = [pc EXCEPT ![self] = "dsa6"] |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, |
| fpsimd_last_state, hwfpsimd, sve_user_trap, |
| stack, next, next_, kval, val >> |
| |
| dsa6(self) == /\ pc[self] = "dsa6" |
| /\ interrupts' = [interrupts EXCEPT ![cpu[self]] = "off"] |
| /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "do_notify_resume", |
| pc |-> "dsa7" ] >> |
| \o stack[self]] |
| /\ pc' = [pc EXCEPT ![self] = "dnr1"] |
| /\ UNCHANGED << cpu, runqueue, in_interrupt, mode, preempt_count, |
| thread, fpsimd_last_state, fpsimd_context_busy, |
| hwfpsimd, sve_user_trap, next, next_, kval, val >> |
| |
| dsa7(self) == /\ pc[self] = "dsa7" |
| /\ mode' = [mode EXCEPT ![self] = "user"] |
| /\ interrupts' = [interrupts EXCEPT ![cpu[self]] = "on"] |
| /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] |
| /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] |
| /\ UNCHANGED << cpu, runqueue, in_interrupt, preempt_count, |
| thread, fpsimd_last_state, fpsimd_context_busy, |
| hwfpsimd, sve_user_trap, next, next_, kval, val >> |
| |
| do_sve_acc(self) == dsa1(self) \/ dsa2(self) \/ dsa3(self) \/ dsa4(self) |
| \/ dsa5(self) \/ dsa6(self) \/ dsa7(self) |
| |
| kn1(self) == /\ pc[self] = "kn1" |
| /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "kernel_neon_begin", |
| pc |-> "kn2" ] >> |
| \o stack[self]] |
| /\ pc' = [pc EXCEPT ![self] = "knb1"] |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, |
| preempt_count, thread, fpsimd_last_state, |
| fpsimd_context_busy, hwfpsimd, sve_user_trap, |
| next, next_, kval, val >> |
| |
| kn2(self) == /\ pc[self] = "kn2" |
| /\ \E v \in VALS: |
| /\ kval' = [kval EXCEPT ![self] = << v, "zero" >>] |
| /\ hwfpsimd' = [hwfpsimd EXCEPT ![cpu[self]] = kval'[self]] |
| /\ pc' = [pc EXCEPT ![self] = "kn3"] |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, |
| preempt_count, thread, fpsimd_last_state, |
| fpsimd_context_busy, sve_user_trap, stack, next, |
| next_, val >> |
| |
| kn3(self) == /\ pc[self] = "kn3" |
| /\ Assert(hwfpsimd[cpu[self]][1] = kval[self][1], |
| "Failure of assertion at line 115, column 9 of macro called at line 354, column 9.") |
| /\ /\ kval' = [kval EXCEPT ![self] = Head(stack[self]).kval] |
| /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "kernel_neon_end", |
| pc |-> Head(stack[self]).pc ] >> |
| \o Tail(stack[self])] |
| /\ pc' = [pc EXCEPT ![self] = "kne1"] |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, |
| preempt_count, thread, fpsimd_last_state, |
| fpsimd_context_busy, hwfpsimd, sve_user_trap, |
| next, next_, val >> |
| |
| kernel_neon(self) == kn1(self) \/ kn2(self) \/ kn3(self) |
| |
| sys_entry(self) == /\ pc[self] = "sys_entry" |
| /\ mode' = [mode EXCEPT ![self] = "kernel"] |
| /\ thread' = [thread EXCEPT ![self].flags = thread[self].flags \ {"TIF_SVE"}] |
| /\ sve_user_trap' = [sve_user_trap EXCEPT ![cpu[self]] = TRUE] |
| /\ pc' = [pc EXCEPT ![self] = "sys1"] |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, |
| preempt_count, fpsimd_last_state, |
| fpsimd_context_busy, hwfpsimd, stack, next, |
| next_, kval, val >> |
| |
| sys1(self) == /\ pc[self] = "sys1" |
| /\ \/ /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "kernel_neon", |
| pc |-> "sys1", |
| kval |-> kval[self] ] >> |
| \o stack[self]] |
| /\ kval' = [kval EXCEPT ![self] = defaultInitValue] |
| /\ pc' = [pc EXCEPT ![self] = "kn1"] |
| \/ /\ pc' = [pc EXCEPT ![self] = "ret_to_user"] |
| /\ UNCHANGED <<stack, kval>> |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, |
| preempt_count, thread, fpsimd_last_state, |
| fpsimd_context_busy, hwfpsimd, sve_user_trap, |
| next, next_, val >> |
| |
| ret_to_user(self) == /\ pc[self] = "ret_to_user" |
| /\ interrupts' = [interrupts EXCEPT ![cpu[self]] = "off"] |
| /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "do_notify_resume", |
| pc |-> "sys2" ] >> |
| \o stack[self]] |
| /\ pc' = [pc EXCEPT ![self] = "dnr1"] |
| /\ UNCHANGED << cpu, runqueue, in_interrupt, mode, |
| preempt_count, thread, fpsimd_last_state, |
| fpsimd_context_busy, hwfpsimd, |
| sve_user_trap, next, next_, kval, val >> |
| |
| sys2(self) == /\ pc[self] = "sys2" |
| /\ mode' = [mode EXCEPT ![self] = "user"] |
| /\ interrupts' = [interrupts EXCEPT ![cpu[self]] = "on"] |
| /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] |
| /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] |
| /\ UNCHANGED << cpu, runqueue, in_interrupt, preempt_count, |
| thread, fpsimd_last_state, fpsimd_context_busy, |
| hwfpsimd, sve_user_trap, next, next_, kval, val >> |
| |
| syscall(self) == sys_entry(self) \/ sys1(self) \/ ret_to_user(self) |
| \/ sys2(self) |
| |
| thr1(self) == /\ pc[self] = "thr1" |
| /\ cpu[self] # "none" |
| /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "fpsimd_restore_current_state", |
| pc |-> "thr2" ] >> |
| \o stack[self]] |
| /\ pc' = [pc EXCEPT ![self] = "frcs1"] |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, |
| preempt_count, thread, fpsimd_last_state, |
| fpsimd_context_busy, hwfpsimd, sve_user_trap, |
| next, next_, kval, val >> |
| |
| thr2(self) == /\ pc[self] = "thr2" |
| /\ interrupts' = [interrupts EXCEPT ![cpu[self]] = "on"] |
| /\ pc' = [pc EXCEPT ![self] = "thr3"] |
| /\ UNCHANGED << cpu, runqueue, in_interrupt, mode, preempt_count, |
| thread, fpsimd_last_state, fpsimd_context_busy, |
| hwfpsimd, sve_user_trap, stack, next, next_, |
| kval, val >> |
| |
| thr3(self) == /\ pc[self] = "thr3" |
| /\ \/ /\ \E v \in VALS: |
| /\ val' = [val EXCEPT ![self] = << v, "zero" >>] |
| /\ hwfpsimd' = [hwfpsimd EXCEPT ![cpu[self]] = val'[self]] |
| /\ pc' = [pc EXCEPT ![self] = "thr3"] |
| /\ stack' = stack |
| \/ /\ Assert(hwfpsimd[cpu[self]][1] = val[self][1], |
| "Failure of assertion at line 115, column 9 of macro called at line 390, column 27.") |
| /\ pc' = [pc EXCEPT ![self] = "thr3"] |
| /\ UNCHANGED <<hwfpsimd, stack, val>> |
| \/ /\ ~sve_user_trap[cpu[self]] |
| /\ \E v \in VALS \X VALS: |
| /\ val' = [val EXCEPT ![self] = v] |
| /\ hwfpsimd' = [hwfpsimd EXCEPT ![cpu[self]] = val'[self]] |
| /\ pc' = [pc EXCEPT ![self] = "thr3"] |
| /\ stack' = stack |
| \/ /\ ~sve_user_trap[cpu[self]] |
| /\ Assert(hwfpsimd[cpu[self]] = val[self], |
| "Failure of assertion at line 124, column 9 of macro called at line 393, column 59.") |
| /\ pc' = [pc EXCEPT ![self] = "thr3"] |
| /\ UNCHANGED <<hwfpsimd, stack, val>> |
| \/ /\ sve_user_trap[cpu[self]] |
| /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "do_sve_acc", |
| pc |-> "thr3" ] >> |
| \o stack[self]] |
| /\ pc' = [pc EXCEPT ![self] = "dsa1"] |
| /\ UNCHANGED <<hwfpsimd, val>> |
| \/ /\ val' = [val EXCEPT ![self][2] = "zero"] |
| /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "syscall", |
| pc |-> "thr3" ] >> |
| \o stack[self]] |
| /\ pc' = [pc EXCEPT ![self] = "sys_entry"] |
| /\ UNCHANGED hwfpsimd |
| /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, |
| preempt_count, thread, fpsimd_last_state, |
| fpsimd_context_busy, sve_user_trap, next, next_, |
| kval >> |
| |
| thread_(self) == thr1(self) \/ thr2(self) \/ thr3(self) |
| |
| (* Allow infinite stuttering to prevent deadlock on termination. *) |
| Terminating == /\ \A self \in ProcSet: pc[self] = "Done" |
| /\ UNCHANGED vars |
| |
| Next == (\E self \in ProcSet: \/ kernel_neon_begin(self) |
| \/ kernel_neon_end(self) |
| \/ fpsimd_restore_current_state(self) |
| \/ fpsimd_thread_switch(self) |
| \/ schedule(self) \/ do_notify_resume(self) |
| \/ interrupt_handler(self) |
| \/ do_sve_acc(self) \/ kernel_neon(self) |
| \/ syscall(self)) |
| \/ (\E self \in THREADS: thread_(self)) |
| \/ Terminating |
| |
| Spec == Init /\ [][Next]_vars |
| |
| Termination == <>(\A self \in ProcSet: pc[self] = "Done") |
| |
| \* END TRANSLATION |
| ------------------------------------------------------------------------------ |
| |
| \* Inject the interrupt_handler call into the call path |
| Interrupt(self) == |
| \* Only interrupt running threads |
| /\ cpu[self] # "none" |
| /\ interrupts[cpu[self]] = "on" |
| \* Non-reentrant interrupt handler |
| /\ ~in_interrupt[self] |
| \* Save the PC of the interrupted context on the stack. |
| /\ stack' = [stack EXCEPT ![self] = << [procedure |-> "interrupt_handler", |
| pc |-> pc[self]] >> |
| \o stack[self]] |
| /\ pc' = [pc EXCEPT ![self] = "handle_int"] |
| /\ UNCHANGED << global_vars, local_vars >> |
| |
| OSNext == (\E self \in THREADS : Interrupt(self)) \/ Next |
| |
| OSSpec == Init /\ [][OSNext]_vars |
| ============================================================================== |
