News
Clarification on the English-language description of Project 01
Written on 07.01.2025 16:46 by Andrea Lattuada
Dear all, I would like to make a small clarification to the English-language description in the handout of Project 1.
Specifically, you should read the fourth paragraph as follows (it is unchanged, except for the part added in bold):
To guard against duplicate messages, the nodes associate a monotonically increasing epoch number with the lock. Initially, node 0 (if present) holds the lock and its epoch number is 1, while all other nodes with an epoch of 0 (and not holding the lock). A node that holds the lock can “grant” it to another node by sending them a “Grant” message which has an epoch number that is greater than the node's epoch number. A node that receives such a message will become the new holder and will set its epoch number to the message’s epoch number. A node should reject (i.e. not receive) lock "Grant" messages with epochs lower or equal to their current epoch, as these are stale (duplicates).
---
Additionally, please note that I believe it is very unlikely that a safety property that is expressed concisely will also be inductive by itself for this protocol. If you did not need any additional conjuncts in your `inv` in addition to `safe` I would strongly recommend carefully inspecting your protocol definition and safety property.
All of this will also be discussed during the tutorial tomorrow.