@@ -303,19 +303,19 @@ Therefore, the proof's correctness relies on the correctness of our models.
303
303
Core C is always allowed to read ` pxCurrentTCBs[C] ` .
304
304
However, writing requires the interrupts on core C to be deactivated.
305
305
306
- - task lock:
307
- The task lock is used to protect ciritical sections and resources from being accessed by multiple tasks simultaneously.
308
-
309
- - ISR lock:
310
- The ISR/ interrupt lock is used to protect critical sections and resources from being accessed by multiple interrupts simultaneously.
311
-
312
- - task lock + ISR lock:
313
- Access to certain resources and ciritical sections are protected by both the task lock and the ISR lock.
314
- For these, it is crucial that we first acquire the task lock and then the ISR lock.
315
- Likewise, we must release them in opposite order.
316
- Failure to comply with this order may lead to deadlocks.
317
- The resources protected by both locks are the main resources this proof deals with.
318
- These include the ready lists and the certain access rights to the tasks' run states.
306
+ - task lock:
307
+ The task lock is used to protect ciritical sections and resources from being accessed by multiple tasks simultaneously.
308
+
309
+ - ISR lock:
310
+ The ISR/ interrupt lock is used to protect critical sections and resources from being accessed by multiple interrupts simultaneously.
311
+
312
+ - task lock + ISR lock:
313
+ Access to certain resources and ciritical sections are protected by both the task lock and the ISR lock.
314
+ For these, it is crucial that we first acquire the task lock and then the ISR lock.
315
+ Likewise, we must release them in opposite order.
316
+ Failure to comply with this order may lead to deadlocks.
317
+ The resources protected by both locks are the main resources this proof deals with.
318
+ These include the ready lists and the certain access rights to the tasks' run states.
319
319
320
320
#### Lock Invariants
321
321
Every synchronization mechanism protects specific data structures and sections of code.
0 commit comments