From c5e6df975d86785899fa5cf3ace86620c7441a0b Mon Sep 17 00:00:00 2001
From: Marco Realacci <marco@marcorealacci.me>
Date: Mon, 17 Mar 2025 22:57:45 +0100
Subject: [PATCH] vault backup: 2025-03-17 22:57:45

---
 .obsidian/workspace.json                      |  4 +-
 .../5 - Software Transactional Memory.md      | 44 ++++++++++++++++++-
 2 files changed, 45 insertions(+), 3 deletions(-)

diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json
index 9fe484b..973d459 100644
--- a/.obsidian/workspace.json
+++ b/.obsidian/workspace.json
@@ -34,9 +34,9 @@
               "type": "pdf",
               "state": {
                 "file": "Concurrent Systems/slides/class 5.pdf",
-                "page": 7,
+                "page": 8,
                 "left": -23,
-                "top": 364,
+                "top": 450,
                 "zoom": 0.652019002375297
               },
               "icon": "lucide-file-text",
diff --git a/Concurrent Systems/notes/5 - Software Transactional Memory.md b/Concurrent Systems/notes/5 - Software Transactional Memory.md
index d272c0f..588b09c 100644
--- a/Concurrent Systems/notes/5 - Software Transactional Memory.md	
+++ b/Concurrent Systems/notes/5 - Software Transactional Memory.md	
@@ -111,4 +111,46 @@ We have m shared MRMW registers; register X is represented by a pair XX, with:
 - XX.val the current value of X
 - XX.depend[1...m] a vector clock s.t.
 	- XX.depend[X] is the sequence number associated with the current value of X
-	- XX.depend[Y] is the sequence number associated with the value of Y on which the current value of X depends from
\ No newline at end of file
+	- XX.depend[Y] is the sequence number associated with the value of Y on which the current value of X depends from
+- There is a starvation-free lock object associated to the pair
+
+We have n processes; process $p_i$ has
+- for every X, a local copy lc(XX) of the implementation of X
+- $p\_depend_i[1…m]$ s.t. $p\_depend_i[X]$ is the seq.num. of the last val of X (directly or undirectly) known by $p_i$
+
+Every transaction T issues by pi has:
+- read_set(T) and write_set(T)
+- $t\_depend_{T}[1…m]$ a local copy of $p\_depend_i$ (this is used in the optimistic execution, not to change $p\_depend_{i}$ if T aborts)
+
+```
+begin_T() :=
+	read_set(T), write_set(T) <- ∅
+	t_depend_T <- p_depend_i
+
+X.read_T() :=
+	if lc?(XX) != ⊥ then
+		return lc(XX).val
+	lc(XX) <- XX
+	if lc(XX).date >= birthdate(T) then
+		ABORT
+	read_set(T) <- read_set(T) U {X}
+	return lc(XX).val
+
+X.write_T(v) :=
+	if lc(XX) = ⊥ then
+		lc(XX) <- newloc
+	lc(XX).val <- v
+	write_set(T) <- write_set(T) U {X}
+
+try_to_commit_T() :=
+	lock all read_set(T) U write_set(T)
+	∀ X ∈ read_set(T)
+		if XX.date >= birthdate(T) then
+			release all locks
+			ABORT
+		tmp <- CLOCK.fetch&add(1)+1
+		∀ X ∈ write_set(T)
+			XX <- ⟨lc(XX).val, tmp⟩
+		release all locks
+		COMMIT
+```
\ No newline at end of file