vault backup: 2025-03-25 13:39:04

This commit is contained in:
Marco Realacci 2025-03-25 13:39:04 +01:00
parent 9e805c5447
commit 103bf38c51

View file

@ -177,7 +177,7 @@ pop() :=
if TOP.compare&set(⟨i,v,s⟩,newtop) then
return v
```
la conclude serve a garantire che il sequence number sia corretto. Se è stato già aggiornato non lo aggiorna.
#### Liveness theorem
the implementation of the stack is non-blocking