diff options
| author | Catalin Marinas <catalin.marinas@arm.com> | 2018-08-10 13:09:34 +0100 |
|---|---|---|
| committer | Catalin Marinas <catalin.marinas@arm.com> | 2018-08-10 13:09:34 +0100 |
| commit | 4e461793535597d80c0af359ba7f9c2c7ec1ccae (patch) | |
| tree | b273bafe0fab99c6a687e75c533e89eb8302adee | |
| parent | 0f8cf64b6733fffa795fef1b2b1f38873db5efd3 (diff) | |
| download | kernel-tla-4e461793535597d80c0af359ba7f9c2c7ec1ccae.tar.gz | |
ctxsw: Introduce an IntCall() action
This replaces the explicit pc/stack manipulation in the Interrupt()
action.
Signed-off-by: Catalin Marinas <catalin.marinas@arm.com>
| -rw-r--r-- | ctxsw.tla | 13 |
1 files changed, 8 insertions, 5 deletions
@@ -632,17 +632,20 @@ Spec == Init /\ [][Next]_vars \* END TRANSLATION ------------------------------------------------------------------------------ +\* Call the given label with the return path set to the interrupted pc and stack +IntCall(self, proc, label) == + /\ stack' = [stack EXCEPT ![self] = << [procedure |-> proc, + pc |-> pc[self]] >> + \o stack[self]] + /\ pc' = [pc EXCEPT ![self] = label] + Interrupt(self) == \* only interrupt running tasks with interrupts enabled /\ Running(self) /\ interrupts[task[self].cpu] = "on" \* non-reentrant handler /\ pc[self] # "handle_irq" - \* IRQ handler call; save the return pc on the stack - /\ stack' = [stack EXCEPT ![self] = << [procedure |-> "interrupt", - pc |-> pc[self]] >> - \o stack[self]] - /\ pc' = [pc EXCEPT ![self] = "handle_irq"] + /\ IntCall(self, "interrupt", "handle_irq") /\ UNCHANGED proc_vars PreemptNext == (\E self \in ProcSet : Interrupt(self)) \/ Next |