vault backup: 2025-03-24 09:48:11

This commit is contained in:
Marco Realacci 2025-03-24 09:48:11 +01:00
parent 78d5af9cda
commit 50df8f7b64
3 changed files with 12 additions and 4 deletions

View file

@ -51,9 +51,9 @@
"type": "pdf", "type": "pdf",
"state": { "state": {
"file": "Concurrent Systems/slides/class 7.pdf", "file": "Concurrent Systems/slides/class 7.pdf",
"page": 5, "page": 8,
"left": -23, "left": -23,
"top": 149, "top": 103,
"zoom": 0.680522565320665 "zoom": 0.680522565320665
}, },
"icon": "lucide-file-text", "icon": "lucide-file-text",
@ -237,6 +237,7 @@
"lastOpenFiles": [ "lastOpenFiles": [
"Concurrent Systems/slides/class 7.pdf", "Concurrent Systems/slides/class 7.pdf",
"Concurrent Systems/notes/7- MUTEX-free concurrency.md", "Concurrent Systems/notes/7- MUTEX-free concurrency.md",
"Pasted image 20250324092633.png",
"Pasted image 20250324091452.png", "Pasted image 20250324091452.png",
"Concurrent Systems/notes/Pasted image 20250324082534.png", "Concurrent Systems/notes/Pasted image 20250324082534.png",
"Concurrent Systems/notes/6a - Alternatives to Atomicity.md", "Concurrent Systems/notes/6a - Alternatives to Atomicity.md",
@ -270,7 +271,6 @@
"HCIW/slides/3Haptic interaction.pdf", "HCIW/slides/3Haptic interaction.pdf",
"HCIW/notes/2 - Interface and Interaction for IoT.md", "HCIW/notes/2 - Interface and Interaction for IoT.md",
"HCIW/notes/3 - Beacons.md", "HCIW/notes/3 - Beacons.md",
"Concurrent Systems/notes/images/Pasted image 20250312121828.png",
"Concurrent Systems/notes/1 - CS Basics2.md", "Concurrent Systems/notes/1 - CS Basics2.md",
"HCIW/notes/1 - UX for IoT.md", "HCIW/notes/1 - UX for IoT.md",
"HCIW/exercises/Exercise.md", "HCIW/exercises/Exercise.md",

View file

@ -93,3 +93,11 @@ get_ts(i) :=
#### Soundness theorem (yes, again) #### Soundness theorem (yes, again)
this implementation satisfies the three properties of the timestamp generator this implementation satisfies the three properties of the timestamp generator
1. Validity holds because of property 2.c of the splitter
2. For consistency, the invocation that terminates increased the value of NEXT before terminating
- every process that starts after its termination will find NEXT to a greater value (NEXT never decreases!)
3. Obstruction freedom is trivial
**REMARK:** this implementation doesnt satisfy the non-blocking property:![[Pasted image 20250324092633.png]]
### A Wait-free Stack

Binary file not shown.

After

Width:  |  Height:  |  Size: 19 KiB