Commit Graph

10 Commits

Author SHA1 Message Date
Ryan Everett
3dd6cde0d8 Mention functional correctness explicitly
Signed-off-by: Ryan Everett <ryan.everett@arm.com>
2023-12-20 16:47:57 +00:00
Ryan Everett
f5e135670b Clarify key generation and memory-management correctness
Signed-off-by: Ryan Everett <ryan.everett@arm.com>
2023-12-20 15:24:47 +00:00
Ryan Everett
c1c6e0d906 Justify linearization points
Signed-off-by: Ryan Everett <ryan.everett@arm.com>
2023-12-15 12:33:26 +00:00
Ryan Everett
6ecb9ce5fc Link directly to the state transition diagram
Signed-off-by: Ryan Everett <ryan.everett@arm.com>
2023-12-14 15:19:31 +00:00
Ryan Everett
acfd774bca 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>
2023-12-14 15:19:31 +00:00
Ryan Everett
3eb4274a57 Fix transitions in diagram
Move the finish_key_creation transition
Neaten the diagram
Add transitions for the key loading functions in psa_get_and_lock_key_slot
Add psa_wipe_key_slot transition
Change file to be a png

Signed-off-by: Ryan Everett <ryan.everett@arm.com>
2023-12-14 15:19:01 +00:00
Ryan Everett
b461b8731c Change how the state transition diagram is stored
Store the source of the diagram as a url instead of an xml file.
Signed-off-by: Ryan Everett <ryan.everett@arm.com>
2023-12-14 14:40:45 +00:00
Ryan Everett
177a45f556 Small clarifications in documentation
Signed-off-by: Ryan Everett <ryan.everett@arm.com>
2023-12-07 11:24:30 +00:00
Ryan Everett
204c852442 Move psa-thread-safety.md
Signed-off-by: Ryan Everett <ryan.everett@arm.com>
2023-12-07 11:05:37 +00:00
Ryan Everett
1e9733c6a8 Add graph
Signed-off-by: Ryan Everett <ryan.everett@arm.com>
2023-12-07 11:05:37 +00:00