vault backup: 2025-03-25 14:51:48

This commit is contained in:
Marco Realacci 2025-03-25 14:51:48 +01:00
parent 408d89472c
commit 31c9dfbc99

View file

@ -184,4 +184,6 @@ the implementation of the stack is non-blocking
*Proof:*
Let us consider an operation invocation performed by p
- if it terminates, √
- otherwise, TOP has changed between the first of TOP and the last Compare&set
- otherwise, TOP has changed between the first of TOP and the last Compare&set
- but the only instruction that modifies TOP is the closing Compare&set
- which means that the invocation issued by another process has terminated! √