Add some clarifications in thread_safety.md

Make it clearer how it is possible to reason here using linearization

Signed-off-by: Ryan Everett <ryan.everett@arm.com>
This commit is contained in:
Ryan Everett 2023-12-14 14:48:43 +00:00
parent 3eb4274a57
commit acfd774bca

View file

@ -292,9 +292,11 @@ To change `slot` to state `new_state`, a function must call `psa_slot_state_tran
A counter field within each slot keeps track of how many readers have registered. Library functions must call `psa_register_read` before reading the key data witin a slot, and `psa_unregister_read` after they have finished operating.
Any call to `psa_slot_state_transition`, `psa_register_read` or `psa_unregister_read` must be performed by a function which holds the global mutex.
Library functions which operate on a slot will return `PSA_ERROR_BAD_STATE` if the slot is in an inappropriate state for the function at the linearization point.
A state transition diagram can be found in docs/architecture/psa-thread-safety/key-slot-state-transitions.jpg. In this diagram, an arrow between two states `q1` and `q2` with label `f` indicates that if the state of a slot is `q1` immediately before `f`'s linearization point, it may be `q2` immediately after `f`'s linearization point. The linearization point of a state changing call to a function must be a call to `psa_slot_state_transition`.
A state transition diagram can be found in docs/architecture/psa-thread-safety/key-slot-state-transitions.png. In this diagram, an arrow between two states `q1` and `q2` with label `f` indicates that if the state of a slot is `q1` immediately before `f`'s linearization point, it may be `q2` immediately after `f`'s linearization point. The linearization point of a state changing call to a function must be a call to `psa_slot_state_transition`. (A function which: locks the global mutex, performs some operation, calls `psa_slot_state_transition` and then unlocks the global mutex, cleans up and returns can satisfy this requirement).
#### Generating the state transition diagram from source