Modeling 5: Concurrent Election and Topsort Revisited
Learning outcomes
In this assignment, you will:
- Continue practicing using temporal logic operators to model a system.
- Use Alloy to demonstrate a counterexample for a buggy algorithm.
- Since this is the last Alloy assignment, you will design these two models from scratch (without stencil files) to practice for open-ended final projects.
This is a pair assignment—you may choose to either complete the assignment alone or with one other CS340 classmate. On Gradescope, you will be able to form a group with maximum size 2.
Because this is the last assignment before Spring Break, it is due next Wednesday instead of next Tuesday (with a late deadline of the Friday before Spring Break). Next week's Workshop will be an optional session to ask additional questions about this same assignment.
Setup
You can run this assignment locally, on your own machine. This assignment uses Alloy 6, as installed in the previous assignments.
Additional Alloy Resources
For additional resources on temporal logic syntax/meaning in Alloy, check out:
AlloyDocs: Time
"Meaning of temporal connectives" in Alloy 6 Documentation
Verifying Expected Properties: Formal Software Design with Alloy 6
It's About Time: Alloy 6 blog post
Task 0: Concurrent election (ungraded, participation credit)
You are a network engineer tasked with designing an algorithm to choose a leader from a specific topology of servers: servers forming a ring.
The scenario is that each server will be part of a distributed system and will run identical code. However, each server has a unique server ID that is a single integer (for our purposes, we will not consider overflow). Each server knows it is in a ring, but does not know how many other servers are in the ring in total.
The servers form a ring where each server can send messages to one neighboring server. The message can consist of any information, but less information is better (since it is lower cost to send).
Your task is to write pseudocode for an algorithm each server can run such that the servers eventually agree on who the next leader is. (
This is a problem with its own Wikipedia page and a long history of solutions based on various constraints, but please wait to check that out until after the Workshop exercise!).
Note: you may not have seen this type of problem before, which is why this is an ungraded exercise. During Workshop, we will work in groups to solve this problem in pseudocode, but you do not need to actually code a solution for this assignment.
Task 1: Modeling concurrent election
Only start on this task after we have completed the workshop exercise! Click to expand.
Since each server has a unique ID that is an integer, some server must have the highest ID (or, equivalently, the lowest ID, but we will proceed using the highest). See the Wikipedia page, noting that this is the common solution when each server has a unique ID.
One basic way to model the algorithm is for each server to track the highest server ID it has seen so far and consider that the leader.
Each server initially sends its own ID to its successor in the ring. Whenever a server receives an ID higher than what it has seen so far, it updates its highest seen ID.
The original ring election papers specify this in slightly different ways.
For example, the Chang & Roberts 1979 paper specifies the algorithm as so:
"Each process is assumed to know its own number, and initially it generates a message with its own number, passing it to the left. A process receiving a message compares the number on the message with its own. If its own number is lower, the process passes the message (to its left). If its own number is higher, the process throws the message away, and if equal, it is the highest numbered process in the system."
You can choose to model any version, as long as it meets the two properties below!
Your task is to model this leadership election in temporal Alloy. Your goal is to show two properties:
1. Eventually, a leader is elected.
2. Once a leader is elected, the leader will not change.
Create your model in a file named ring_election.als. Your file should have at least two check statements, one for each property above. You should also have at least one run statement that shows a successful election on a ring of at least 3 servers.
I suggest following the design we saw in the mutex example, where transition predicates apply to a single server and all server take some transition predicate in every step. Each server should be allowed to do nothing in an arbitrary step, but if the election is not over, each server should eventually take an action transition predicate in order for the algorithm to make progress.
Some other design suggestions:
- Make sure overflows are prevented in the Alloy settings.
- You do not need to explicitly model servers "knowing" the election has been won (though you may choose to do so). Rather, the election can be considered won as soon as every server has the same notion of the highest ID within the network.
README
Start a README and answer the following written questions there:
Written Q1: Describe your model as if this were a publicly-viewable README. The length should be 1-2 paragraphs.
Note that the textbook covers a more complicated version of this problem. The model is different enough that it is unlikely to be helpful in designing your own model using temporal logic.
Task 2: Buggy topsort
Alice attempted to write out pseudocode for topological sort without checking her CS340 notes.
She came up with the following algorithm:
L ← Empty list that will contain the sorted elements
S ← Set of all nodes with no incoming edges
while S is non-empty do
remove a node n from S
add n to tail of L
for each node m with an edge e from n to m do
remove edge e from the graph
insert m into S
return L
You will use Alloy to demonstrate the problem with this algorithm.
Buggy
Your task is to model this algorithm in temporal Alloy.
Create your initial model in a file named buggy_topsort.als. Your model should have:
- A
check statement that shows that Alice's buggy algorithm can fail to produce a correct topological sort.
- A
run statement that shows Alice's algorithm running on a graph with at least 3 edges.
Some design suggestions:
- You can assume the input graph is a DAG (hint: should you encode assumptions in the model as
fact or pred?).
- While you can use any type you'd like for
L and S, you may find it useful to model L as an Alloy sequence (seq). seq Vertex is a shorthand for Int->Vertex where each integer is an index mapped to some vertex. Alloy's seq is documented here; the only methods you may need to use are:
L.add[...]: returns a new list that is L with one element added to the end.L.indexOf[...]: returns the integer index of an element in L, or the empty set if the element is not in L.#L: returns the number of elements in L.
- Your
init predicate can include the first two lines of Alice's pseudocode (that is, S does not need to be empty and can instead be initialized to match that line of the pseudocode).
- Since temporal Alloy only finds lasso traces, this is a model where it is convenient to have a transition predicate that models "do nothing once the loop is over". The precondition for this predicate should match when Alice's pseudocode would break out of the
while loop.
Written Q2: Describe the counterexample(s) Alloy found for the buggy version of topsort. Include both the pattern you saw in the Alloy instance traces and the corresponding incorrect line(s) in the buggy pseudocode.
Now, update your model to show that the correct algorithm does not have the same counterexample(s).
Copy and paste your model to a new file, correct_topsort.als. Update your transition predicates to model the correct algorithm instead.
Written Q3: Describe your model as if this were a publicly-viewable README. Include both the buggy and correct algorithms. The length should be 1-2 paragraphs.
Grading
In your README, also report:
Written Q4: Collaborators other than your partner?
Written Q5: Roughly how long did this assignment take you (in hours)?
This assignment is worth 100 points, broken down by:
40 points: Leader election
- 20: model design (not over- or under-constrained for the algorithm as listed).
- 10: election eventually won predicate and assertion.
- 10: leader does not change once the election is won predicate and assertion.
40 points: Buggy topsort
- 10: static model design (not over- or under-constrained for the algorithm as listed).
- 15: variable model design and transition predicates (not over- or under-constrained for the algorithm as listed).
- 15: correctness predicate and assertion.
10 points: Correct version of Topsort
10 points: README/Written Qs 1-5
Submission
Submit the following 4 files on Gradescope: ring_election.als, buggy_topsort.als, correct_topsort.als, and README.{txt, md}.
Attribution
Task 1 is adapted from Daniel Jackson's Software Abstractions book and a previous version of a Forge Model Checking assignment from Tim Nelson's Logic for Systems at Brown University. Task 2 and 3 are also adapted from Logic for Systems.
Modeling 5: Concurrent Election and Topsort Revisited
Learning outcomes
In this assignment, you will:
This is a pair assignment—you may choose to either complete the assignment alone or with one other CS340 classmate. On Gradescope, you will be able to form a group with maximum size 2.
Because this is the last assignment before Spring Break, it is due next Wednesday instead of next Tuesday (with a late deadline of the Friday before Spring Break). Next week's Workshop will be an optional session to ask additional questions about this same assignment.
Setup
You can run this assignment locally, on your own machine. This assignment uses Alloy 6, as installed in the previous assignments.
Additional Alloy Resources
For additional resources on temporal logic syntax/meaning in Alloy, check out:
AlloyDocs: Time
"Meaning of temporal connectives" in Alloy 6 Documentation
Verifying Expected Properties: Formal Software Design with Alloy 6
It's About Time: Alloy 6 blog post
Task 0: Concurrent election (ungraded, participation credit)
You are a network engineer tasked with designing an algorithm to choose a leader from a specific topology of servers: servers forming a ring.
The scenario is that each server will be part of a distributed system and will run identical code. However, each server has a unique server ID that is a single integer (for our purposes, we will not consider overflow). Each server knows it is in a ring, but does not know how many other servers are in the ring in total.
The servers form a ring where each server can send messages to one neighboring server. The message can consist of any information, but less information is better (since it is lower cost to send).
Your task is to write pseudocode for an algorithm each server can run such that the servers eventually agree on who the next leader is. (
This is a problem with its own Wikipedia page and a long history of solutions based on various constraints, but please wait to check that out until after the Workshop exercise!).
Note: you may not have seen this type of problem before, which is why this is an ungraded exercise. During Workshop, we will work in groups to solve this problem in pseudocode, but you do not need to actually code a solution for this assignment.
Task 1: Modeling concurrent election
Only start on this task after we have completed the workshop exercise! Click to expand.
Since each server has a unique ID that is an integer, some server must have the highest ID (or, equivalently, the lowest ID, but we will proceed using the highest). See the Wikipedia page, noting that this is the common solution when each server has a unique ID.
One basic way to model the algorithm is for each server to track the highest server ID it has seen so far and consider that the leader.
Each server initially sends its own ID to its successor in the ring. Whenever a server receives an ID higher than what it has seen so far, it updates its highest seen ID.
For example, the Chang & Roberts 1979 paper specifies the algorithm as so:
"Each process is assumed to know its own number, and initially it generates a message with its own number, passing it to the left. A process receiving a message compares the number on the message with its own. If its own number is lower, the process passes the message (to its left). If its own number is higher, the process throws the message away, and if equal, it is the highest numbered process in the system."
You can choose to model any version, as long as it meets the two properties below!
Your task is to model this leadership election in temporal Alloy. Your goal is to show two properties:
1. Eventually, a leader is elected.
2. Once a leader is elected, the leader will not change.
Create your model in a file named
ring_election.als. Your file should have at least twocheckstatements, one for each property above. You should also have at least onerunstatement that shows a successful election on a ring of at least 3 servers.I suggest following the design we saw in the mutex example, where transition predicates apply to a single server and all server take some transition predicate in every step. Each server should be allowed to do nothing in an arbitrary step, but if the election is not over, each server should eventually take an action transition predicate in order for the algorithm to make progress.
Some other design suggestions:
README
Start a
READMEand answer the following written questions there:Written Q1: Describe your model as if this were a publicly-viewable README. The length should be 1-2 paragraphs.
Note that the textbook covers a more complicated version of this problem. The model is different enough that it is unlikely to be helpful in designing your own model using temporal logic.
Task 2: Buggy topsort
Alice attempted to write out pseudocode for topological sort without checking her CS340 notes.
She came up with the following algorithm:
You will use Alloy to demonstrate the problem with this algorithm.
Buggy
Your task is to model this algorithm in temporal Alloy.
Create your initial model in a file named
buggy_topsort.als. Your model should have:checkstatement that shows that Alice's buggy algorithm can fail to produce a correct topological sort.runstatement that shows Alice's algorithm running on a graph with at least 3 edges.Some design suggestions:
factorpred?).LandS, you may find it useful to modelLas an Alloy sequence (seq).seq Vertexis a shorthand forInt->Vertexwhere each integer is an index mapped to some vertex. Alloy'sseqis documented here; the only methods you may need to use are:L.add[...]: returns a new list that isLwith one element added to the end.L.indexOf[...]: returns the integer index of an element inL, or the empty set if the element is not inL.#L: returns the number of elements inL.initpredicate can include the first two lines of Alice's pseudocode (that is,Sdoes not need to be empty and can instead be initialized to match that line of the pseudocode).whileloop.Written Q2: Describe the counterexample(s) Alloy found for the buggy version of topsort. Include both the pattern you saw in the Alloy instance traces and the corresponding incorrect line(s) in the buggy pseudocode.
Now, update your model to show that the correct algorithm does not have the same counterexample(s).
Copy and paste your model to a new file,
correct_topsort.als. Update your transition predicates to model the correct algorithm instead.Written Q3: Describe your model as if this were a publicly-viewable README. Include both the buggy and correct algorithms. The length should be 1-2 paragraphs.
Grading
In your README, also report:
Written Q4: Collaborators other than your partner?
Written Q5: Roughly how long did this assignment take you (in hours)?
This assignment is worth 100 points, broken down by:
40 points: Leader election
40 points: Buggy topsort
10 points: Correct version of Topsort
10 points:
README/Written Qs 1-5Submission
Submit the following 4 files on Gradescope:
ring_election.als,buggy_topsort.als,correct_topsort.als, andREADME.{txt, md}.Attribution
Task 1 is adapted from Daniel Jackson's Software Abstractions book and a previous version of a Forge Model Checking assignment from Tim Nelson's Logic for Systems at Brown University. Task 2 and 3 are also adapted from Logic for Systems.