fpsimd: Add SVE support

Model the SVE state access. Software signals are not handled yet.

Signed-off-by: Catalin Marinas <catalin.marinas@arm.com>

1 files changed, 275 insertions, 82 deletions

diff --git a/fpsimd.tla b/fpsimd.tla
index 4396325..0800167 100644
--- a/fpsimd.tla
+++ b/fpsimd.tla
@@ -26,8 +26,9 @@ variables
 
 	\* Thread state
 	thread		= [t \in THREADS |->
-				[fpsimd		|-> << "zero", "zero" >>,
+				[fpsimd_state	|-> "zero",
 				 fpsimd_cpu	|-> "none",
+				 sve_state	|-> << "zero", "zero" >>,
 				 flags		|-> {"TIF_FOREIGN_FPSTATE"}]];
 
 	\* FPSIMD state tracking
@@ -36,16 +37,19 @@ variables
 
 	\* 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"}) \X (VALS \cup {"zero"})
+	FPSIMDType == VALS \cup {"zero"}
+	SVEType == FPSIMDType \X FPSIMDType
 	ThreadStateType ==
-		[fpsimd:	FPSIMDType,
+		[fpsimd_state:	FPSIMDType,
 		 fpsimd_cpu:	CPUS \cup {"none"},
+		 sve_state:	SVEType,
 		 flags:		SUBSET ThreadFlags]
 	TypeInv ==
 		/\ thread \in [THREADS -> ThreadStateType]
@@ -55,7 +59,8 @@ define {
 		/\ cpu \in [THREADS -> CPUS \cup {"none"}]
 		/\ preempt_count \in [THREADS -> Nat]
 		/\ mode \in [THREADS -> {"user", "kernel"}]
-		/\ hwfpsimd \in [CPUS -> FPSIMDType]
+		/\ hwfpsimd \in [CPUS -> SVEType]
+		/\ sve_user_trap \in [CPUS -> BOOLEAN]
 		/\ fpsimd_last_state \in [CPUS -> THREADS \cup {"null"}]
 		/\ fpsimd_context_busy \in [CPUS -> BOOLEAN]
 
@@ -156,27 +161,64 @@ macro put_cpu_fpsimd_context()
 }
 
 macro fpsimd_save_state() {
-	thread[self].fpsimd := hwfpsimd[cpu[self]];
+	thread[self].fpsimd_state := hwfpsimd[cpu[self]][1];
 }
 
 macro fpsimd_load_state() {
-	hwfpsimd[cpu[self]] := thread[self].fpsimd;
+	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)
-		fpsimd_save_state();
+	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]];
-	fpsimd_load_state();
+	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() {
@@ -184,6 +226,11 @@ macro fpsimd_flush_cpu_state() {
 	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();
@@ -280,6 +327,25 @@ int1:	in_interrupt[self] := FALSE;
 	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;
 {
@@ -294,6 +360,7 @@ procedure syscall()
 {
 sys_entry:
 	mode[self] := "kernel";
+	sve_user_discard();
 	\* exercise in-kernel FPSIMD
 sys1:	while (TRUE) {
 		either	call kernel_neon();
@@ -318,26 +385,35 @@ thr1:	\* wait to be scheduled (simulate thread creation)
 thr2:	interrupts_enable();
 thr3:	\* user thread actions
 	while (TRUE) {
-		either	with (v \in VALS) write_fpsimd(v, val);
-		or	read_fpsimd(val);
-		or	call syscall();
+		\* 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 311 col 1 changed to thread_
-\* Procedure variable next of procedure schedule at line 229 col 19 changed to next_
+\* 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, pc, stack
+          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"}) \X (VALS \cup {"zero"})
+FPSIMDType == VALS \cup {"zero"}
+SVEType == FPSIMDType \X FPSIMDType
 ThreadStateType ==
-        [fpsimd:        FPSIMDType,
+        [fpsimd_state:  FPSIMDType,
          fpsimd_cpu:    CPUS \cup {"none"},
+         sve_state:     SVEType,
          flags:         SUBSET ThreadFlags]
 TypeInv ==
         /\ thread \in [THREADS -> ThreadStateType]
@@ -347,7 +423,8 @@ TypeInv ==
         /\ cpu \in [THREADS -> CPUS \cup {"none"}]
         /\ preempt_count \in [THREADS -> Nat]
         /\ mode \in [THREADS -> {"user", "kernel"}]
-        /\ hwfpsimd \in [CPUS -> FPSIMDType]
+        /\ hwfpsimd \in [CPUS -> SVEType]
+        /\ sve_user_trap \in [CPUS -> BOOLEAN]
         /\ fpsimd_last_state \in [CPUS -> THREADS \cup {"null"}]
         /\ fpsimd_context_busy \in [CPUS -> BOOLEAN]
 
@@ -366,7 +443,7 @@ Perms == Permutations(CPUS) \cup Permutations(THREADS) \cup
 
 VARIABLES next, next_, kval, val
 
-global_vars == << hwfpsimd, mode, fpsimd_last_state, preempt_count, fpsimd_context_busy, thread, cpu, in_interrupt, interrupts, runqueue >>
+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 >>
 
@@ -383,12 +460,14 @@ Init == (* Global variables *)
         /\ mode = [t \in THREADS |-> "user"]
         /\ preempt_count = [t \in THREADS |-> 0]
         /\ thread = [t \in THREADS |->
-                          [fpsimd         |-> << "zero", "zero" >>,
+                          [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 *)
@@ -403,25 +482,27 @@ Init == (* Global variables *)
 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 136, column 9 of macro called at line 189, column 9.")
+                        "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, stack, next, 
-                              next_, kval, val >>
+                              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 167, column 9 of macro called at line 190, column 9.")
+                        "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 /\ thread' = [thread EXCEPT ![self].fpsimd = hwfpsimd[cpu[self]]]
+                    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, stack, next, 
-                              next_, kval, val >>
+                              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"]
@@ -430,32 +511,32 @@ knb3(self) == /\ pc[self] = "knb3"
               /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
               /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, 
                               preempt_count, fpsimd_context_busy, hwfpsimd, 
-                              next, next_, kval, val >>
+                              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 142, column 9 of macro called at line 197, column 9.")
+                        "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, next, next_, 
-                              kval, val >>
+                              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 136, column 9 of macro called at line 203, column 9.")
+                         "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, stack, 
-                               next, next_, kval, val >>
+                               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
@@ -465,15 +546,20 @@ frcs2(self) == /\ pc[self] = "frcs2"
                           /\ UNCHANGED thread
                /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, 
                                preempt_count, fpsimd_last_state, 
-                               fpsimd_context_busy, hwfpsimd, stack, next, 
-                               next_, kval, val >>
+                               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 173, column 9 of macro called at line 206, column 17.")
-               /\ hwfpsimd' = [hwfpsimd EXCEPT ![cpu[self]] = thread[self].fpsimd]
+                         "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, 
@@ -481,32 +567,34 @@ frcs3(self) == /\ pc[self] = "frcs3"
 
 frcs4(self) == /\ pc[self] = "frcs4"
                /\ Assert(fpsimd_context_busy[cpu[self]], 
-                         "Failure of assertion at line 142, column 9 of macro called at line 209, column 9.")
+                         "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, next, 
-                               next_, kval, val >>
+                               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 136, column 9 of macro called at line 216, column 9.")
+                        "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 167, column 9 of macro called at line 217, column 9.")
+                        "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 /\ thread' = [thread EXCEPT ![self].fpsimd = hwfpsimd[cpu[self]]]
+                    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, 
-                              stack, next, next_, kval, val >>
+                              sve_user_trap, stack, next, next_, kval, val >>
 
 fts2(self) == /\ pc[self] = "fts2"
               /\ IF fpsimd_last_state[cpu[self]] # next[self] \/
@@ -516,27 +604,27 @@ fts2(self) == /\ pc[self] = "fts2"
               /\ pc' = [pc EXCEPT ![self] = "fts3"]
               /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, 
                               preempt_count, fpsimd_last_state, 
-                              fpsimd_context_busy, hwfpsimd, stack, next, 
-                              next_, kval, val >>
+                              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 142, column 9 of macro called at line 224, column 9.")
+                        "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, next_, kval, val >>
+                              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 231, column 9.")
+                        "Failure of assertion at line 278, column 9.")
               /\ Assert(interrupts[cpu[self]] = "off", 
-                        "Failure of assertion at line 232, column 9.")
+                        "Failure of assertion at line 279, column 9.")
               /\ \E n \in runqueue \cup {"none"}:
                    IF n = "none"
                       THEN /\ interrupts' = [interrupts EXCEPT ![cpu[self]] = "on"]
@@ -550,7 +638,7 @@ sch1(self) == /\ pc[self] = "sch1"
                            /\ UNCHANGED << interrupts, stack >>
               /\ UNCHANGED << cpu, in_interrupt, mode, preempt_count, thread, 
                               fpsimd_last_state, fpsimd_context_busy, hwfpsimd, 
-                              next, kval, val >>
+                              sve_user_trap, next, kval, val >>
 
 sch2(self) == /\ pc[self] = "sch2"
               /\ /\ next' = [next EXCEPT ![self] = next_[self]]
@@ -561,7 +649,8 @@ sch2(self) == /\ pc[self] = "sch2"
               /\ pc' = [pc EXCEPT ![self] = "fts1"]
               /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, 
                               preempt_count, thread, fpsimd_last_state, 
-                              fpsimd_context_busy, hwfpsimd, next_, kval, val >>
+                              fpsimd_context_busy, hwfpsimd, sve_user_trap, 
+                              next_, kval, val >>
 
 sch3(self) == /\ pc[self] = "sch3"
               /\ runqueue' = (runqueue \cup {self})
@@ -570,15 +659,16 @@ sch3(self) == /\ pc[self] = "sch3"
               /\ pc' = [pc EXCEPT ![self] = "sch4"]
               /\ UNCHANGED << interrupts, in_interrupt, mode, preempt_count, 
                               thread, fpsimd_last_state, fpsimd_context_busy, 
-                              hwfpsimd, stack, next, next_, kval, val >>
+                              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, stack, next, 
-                              next_, kval, val >>
+                              fpsimd_context_busy, hwfpsimd, sve_user_trap, 
+                              stack, next, next_, kval, val >>
 
 sch5(self) == /\ pc[self] = "sch5"
               /\ interrupts' = [interrupts EXCEPT ![cpu[self]] = "on"]
@@ -587,14 +677,14 @@ sch5(self) == /\ pc[self] = "sch5"
               /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
               /\ UNCHANGED << cpu, runqueue, in_interrupt, mode, preempt_count, 
                               thread, fpsimd_last_state, fpsimd_context_busy, 
-                              hwfpsimd, next, kval, val >>
+                              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 256, column 9.")
+                        "Failure of assertion at line 303, column 9.")
               /\ stack' = [stack EXCEPT ![self] = << [ procedure |->  "schedule",
                                                        pc        |->  "dnr2",
                                                        next_     |->  next_[self] ] >>
@@ -603,7 +693,8 @@ dnr1(self) == /\ pc[self] = "dnr1"
               /\ pc' = [pc EXCEPT ![self] = "sch1"]
               /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, 
                               preempt_count, thread, fpsimd_last_state, 
-                              fpsimd_context_busy, hwfpsimd, next, kval, val >>
+                              fpsimd_context_busy, hwfpsimd, sve_user_trap, 
+                              next, kval, val >>
 
 dnr2(self) == /\ pc[self] = "dnr2"
               /\ IF "TIF_FOREIGN_FPSTATE" \in thread[self].flags
@@ -615,8 +706,8 @@ dnr2(self) == /\ pc[self] = "dnr2"
                          /\ stack' = stack
               /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, 
                               preempt_count, thread, fpsimd_last_state, 
-                              fpsimd_context_busy, hwfpsimd, next, next_, kval, 
-                              val >>
+                              fpsimd_context_busy, hwfpsimd, sve_user_trap, 
+                              next, next_, kval, val >>
 
 dnr3(self) == /\ pc[self] = "dnr3"
               /\ interrupts' = [interrupts EXCEPT ![cpu[self]] = "off"]
@@ -627,7 +718,7 @@ dnr3(self) == /\ pc[self] = "dnr3"
                          /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
               /\ UNCHANGED << cpu, runqueue, in_interrupt, mode, preempt_count, 
                               thread, fpsimd_last_state, fpsimd_context_busy, 
-                              hwfpsimd, next, next_, kval, val >>
+                              hwfpsimd, sve_user_trap, next, next_, kval, val >>
 
 do_notify_resume(self) == dnr1(self) \/ dnr2(self) \/ dnr3(self)
 
@@ -651,7 +742,7 @@ handle_int(self) == /\ pc[self] = "handle_int"
                                           /\ UNCHANGED << stack, next_ >>
                     /\ UNCHANGED << cpu, runqueue, mode, preempt_count, thread, 
                                     fpsimd_last_state, fpsimd_context_busy, 
-                                    hwfpsimd, next, kval, val >>
+                                    hwfpsimd, sve_user_trap, next, kval, val >>
 
 int1(self) == /\ pc[self] = "int1"
               /\ in_interrupt' = [in_interrupt EXCEPT ![self] = FALSE]
@@ -660,10 +751,86 @@ int1(self) == /\ pc[self] = "int1"
               /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
               /\ UNCHANGED << cpu, runqueue, mode, preempt_count, thread, 
                               fpsimd_last_state, fpsimd_context_busy, hwfpsimd, 
-                              next, next_, kval, val >>
+                              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" ] >>
@@ -671,8 +838,8 @@ kn1(self) == /\ pc[self] = "kn1"
              /\ pc' = [pc EXCEPT ![self] = "knb1"]
              /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, 
                              preempt_count, thread, fpsimd_last_state, 
-                             fpsimd_context_busy, hwfpsimd, next, next_, kval, 
-                             val >>
+                             fpsimd_context_busy, hwfpsimd, sve_user_trap, 
+                             next, next_, kval, val >>
 
 kn2(self) == /\ pc[self] = "kn2"
              /\ \E v \in VALS:
@@ -681,11 +848,12 @@ kn2(self) == /\ pc[self] = "kn2"
              /\ pc' = [pc EXCEPT ![self] = "kn3"]
              /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, 
                              preempt_count, thread, fpsimd_last_state, 
-                             fpsimd_context_busy, stack, next, next_, val >>
+                             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 110, column 9 of macro called at line 288, column 9.")
+                       "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 ] >>
@@ -693,15 +861,18 @@ kn3(self) == /\ pc[self] = "kn3"
              /\ pc' = [pc EXCEPT ![self] = "kne1"]
              /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, 
                              preempt_count, thread, fpsimd_last_state, 
-                             fpsimd_context_busy, hwfpsimd, next, next_, val >>
+                             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, thread, fpsimd_last_state, 
+                                   preempt_count, fpsimd_last_state, 
                                    fpsimd_context_busy, hwfpsimd, stack, next, 
                                    next_, kval, val >>
 
@@ -716,7 +887,8 @@ sys1(self) == /\ pc[self] = "sys1"
                     /\ UNCHANGED <<stack, kval>>
               /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, 
                               preempt_count, thread, fpsimd_last_state, 
-                              fpsimd_context_busy, hwfpsimd, next, next_, val >>
+                              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"]
@@ -726,8 +898,8 @@ ret_to_user(self) == /\ pc[self] = "ret_to_user"
                      /\ pc' = [pc EXCEPT ![self] = "dnr1"]
                      /\ UNCHANGED << cpu, runqueue, in_interrupt, mode, 
                                      preempt_count, thread, fpsimd_last_state, 
-                                     fpsimd_context_busy, hwfpsimd, next, 
-                                     next_, kval, val >>
+                                     fpsimd_context_busy, hwfpsimd, 
+                                     sve_user_trap, next, next_, kval, val >>
 
 sys2(self) == /\ pc[self] = "sys2"
               /\ mode' = [mode EXCEPT ![self] = "user"]
@@ -736,7 +908,7 @@ sys2(self) == /\ pc[self] = "sys2"
               /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
               /\ UNCHANGED << cpu, runqueue, in_interrupt, preempt_count, 
                               thread, fpsimd_last_state, fpsimd_context_busy, 
-                              hwfpsimd, next, next_, kval, val >>
+                              hwfpsimd, sve_user_trap, next, next_, kval, val >>
 
 syscall(self) == sys_entry(self) \/ sys1(self) \/ ret_to_user(self)
                     \/ sys2(self)
@@ -749,15 +921,16 @@ thr1(self) == /\ pc[self] = "thr1"
               /\ pc' = [pc EXCEPT ![self] = "frcs1"]
               /\ UNCHANGED << cpu, runqueue, interrupts, in_interrupt, mode, 
                               preempt_count, thread, fpsimd_last_state, 
-                              fpsimd_context_busy, hwfpsimd, next, next_, kval, 
-                              val >>
+                              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, stack, next, next_, kval, val >>
+                              hwfpsimd, sve_user_trap, stack, next, next_, 
+                              kval, val >>
 
 thr3(self) == /\ pc[self] = "thr3"
               /\ \/ /\ \E v \in VALS:
@@ -766,17 +939,36 @@ thr3(self) == /\ pc[self] = "thr3"
                     /\ pc' = [pc EXCEPT ![self] = "thr3"]
                     /\ stack' = stack
                  \/ /\ Assert(hwfpsimd[cpu[self]][1] = val[self][1], 
-                              "Failure of assertion at line 110, column 9 of macro called at line 322, column 25.")
+                              "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>>
-                 \/ /\ stack' = [stack EXCEPT ![self] = << [ procedure |->  "syscall",
+                 \/ /\ ~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] = "sys_entry"]
+                    /\ 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, next, next_, kval >>
+                              fpsimd_context_busy, sve_user_trap, next, next_, 
+                              kval >>
 
 thread_(self) == thr1(self) \/ thr2(self) \/ thr3(self)
 
@@ -786,7 +978,8 @@ Next == (\E self \in ProcSet:  \/ kernel_neon_begin(self)
                                \/ fpsimd_thread_switch(self)
                                \/ schedule(self) \/ do_notify_resume(self)
                                \/ interrupt_handler(self)
-                               \/ kernel_neon(self) \/ syscall(self))
+                               \/ do_sve_acc(self) \/ kernel_neon(self)
+                               \/ syscall(self))
            \/ (\E self \in THREADS: thread_(self))
            \/ (* Disjunct to prevent deadlock on termination *)
               ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)