softirq-read respectively, and the character displayed in each
indicates:
- '.' acquired while irqs enabled
+ '.' acquired while irqs disabled
'+' acquired in irq context
- '-' acquired in process context with irqs disabled
- '?' read-acquired both with irqs enabled and in irq context
+ '-' acquired with irqs enabled
+ '?' read acquired in irq context with irqs enabled.
Unused mutexes cannot be part of the cause of an error.
The validator achieves perfect, mathematical 'closure' (proof of locking
correctness) in the sense that for every simple, standalone single-task
-locking sequence that occured at least once during the lifetime of the
+locking sequence that occurred at least once during the lifetime of the
kernel, the validator proves it with a 100% certainty that no
combination and timing of these locking sequences can cause any class of
lock related deadlock. [*]