diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index b39b803..2827bcd 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -51,9 +51,9 @@ "type": "pdf", "state": { "file": "Concurrent Systems/slides/class 7.pdf", - "page": 5, + "page": 8, "left": -23, - "top": 149, + "top": 103, "zoom": 0.680522565320665 }, "icon": "lucide-file-text", @@ -237,6 +237,7 @@ "lastOpenFiles": [ "Concurrent Systems/slides/class 7.pdf", "Concurrent Systems/notes/7- MUTEX-free concurrency.md", + "Pasted image 20250324092633.png", "Pasted image 20250324091452.png", "Concurrent Systems/notes/Pasted image 20250324082534.png", "Concurrent Systems/notes/6a - Alternatives to Atomicity.md", @@ -270,7 +271,6 @@ "HCIW/slides/3Haptic interaction.pdf", "HCIW/notes/2 - Interface and Interaction for IoT.md", "HCIW/notes/3 - Beacons.md", - "Concurrent Systems/notes/images/Pasted image 20250312121828.png", "Concurrent Systems/notes/1 - CS Basics2.md", "HCIW/notes/1 - UX for IoT.md", "HCIW/exercises/Exercise.md", diff --git a/Concurrent Systems/notes/7- MUTEX-free concurrency.md b/Concurrent Systems/notes/7- MUTEX-free concurrency.md index 09dd627..9aadb47 100644 --- a/Concurrent Systems/notes/7- MUTEX-free concurrency.md +++ b/Concurrent Systems/notes/7- MUTEX-free concurrency.md @@ -92,4 +92,12 @@ get_ts(i) := ``` #### Soundness theorem (yes, again) -this implementation satisfies the three properties of the timestamp generator \ No newline at end of file +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 doesn’t satisfy the non-blocking property:![[Pasted image 20250324092633.png]] + +### A Wait-free Stack diff --git a/Pasted image 20250324092633.png b/Pasted image 20250324092633.png new file mode 100644 index 0000000..afa5075 Binary files /dev/null and b/Pasted image 20250324092633.png differ