vault backup: 2025-03-31 09:15:43

This commit is contained in:
Marco Realacci 2025-03-31 09:15:43 +02:00
parent 9dbe5e30cb
commit 051b47564b

View file

@ -43,6 +43,8 @@ Let us first concentrate on obj's with deterministic specifications (we will see
A process $p_i$ that wants to invoke operation op of object Z with arguments args locally runs:
```
on the foreground thread of pi:
result_i <-
invoc_i <- op(args) , i
wait result_i != ⊥
@ -59,6 +61,8 @@ Let CONS be an unbounded array of consensus objects and 𝜋1 and 𝜋2 respecti
The local simulation of Z by $p_i$ is
```
on the background thread of pi:
k <- 0
z_i <- Z.init()
while true
@ -72,13 +76,12 @@ while true
```
This solution is non-blocking but not wait-free (can run forever).
P.S. *invoc_i*, *result_i* e *z_i* sono variabili locali.
### A wait-free construction
- `LAST_OP[1..n]:` array of SWMR atomic R/W registers containing pairs init at ⟨⊥,0⟩ ∀i
- è condiviso e ogni processo ci infila le sue proposal
- `last_sn_i[1..n]:` local array of the last op by $p_j$ executed by $p_i$ init at 0 ∀i,j
- ogni processo ha la sua copia locale
- `last_sn_i[j]` traccia dell'ultima operazione eseguita da j
- `last_sn_i[j]` tiene traccia dell'ultima operazione eseguita da j
Idea: instead of just proposing my proposal, at every moment I propose all the proposals of all the processes.
@ -89,21 +92,27 @@ or(arg) by p_i on Z
wait result_i != ⊥
return result_i
l'idea è che scrivo la mia proposal sulla shared memory, così ogni processo può leggere la mia proposal.
local simulation of Z by p_i
k <- 0
z_i <- Z.init()
while true
invoc_i <- 𝜀
∀ j = 1..n
if 𝜋2(LAST_OP[j])>last_sni[j] then
invoci.append( ⟨𝜋1(LAST_OP[j]),j⟩ )
if invoci ≠ 𝜀 then
k++
exec_i <- CONS[k].propose(invoci)
for r=1 to |execi|
⟨zi,res⟩ -> 𝛿(zi,𝜋1(execi[r]))
j <- 𝜋2(execi[r])
last_sni[j]++
if i=j then
result_i <- res
if 𝜋2(LAST_OP[j]) > last_sn_i[j] then
# j ha fatto una nuova proposta
invoc_i.append(⟨𝜋1(LAST_OP[j]),j⟩)
# allora la aggiungo alla mia lista invoc_i
if invoci ≠ 𝜀 then
k++
exec_i <- CONS[k].propose(invoci)
for r=1 to |execi|
⟨zi,res⟩ -> 𝛿(zi,𝜋1(execi[r]))
j <- 𝜋2(execi[r])
last_sni[j]++
if i=j then
result_i <- res
```
As before, they are executed by each process on two threads.