Modeling 5: Concurrency and Topsort Revisited
------

# Learning outcomes

:::info
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.
:::

:::warning
This is a **individual assignment**. However, no problems are **[Independent]**, so you can collaborate with other students following the guidelines in the syllabus.
:::

:::success
Because this is the last assignment before Spring Break, it's up to you whether to finish it before the break or after the break.
:::

# Setup

You can run this assignment locally, on your own machine. This assignment uses [Alloy 6](https://alloytools.org/alloy6.html), as installed in the previous assignments. There are no starter/stencil files for this assignment, you will be designing your models from scratch.

## Additional Alloy Resources

For additional resources on temporal logic syntax/meaning in Alloy, check out:

[AlloyDocs: Time](https://alloy.readthedocs.io/en/latest/language/time.html)
["Meaning of temporal connectives" in Alloy 6 Documentation](https://alloytools.org/alloy6.html)
[Verifying Expected Properties: Formal Software Design with Alloy 6](https://haslab.github.io/formal-software-design/overview/index.html#verifying-expected-properties)
[It's About Time: Alloy 6 blog post](https://www.hillelwayne.com/post/alloy6/)

# Task 1: Modeling concurrent election

Imagine 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).

Pause and think about an algorithm each server can run such that the servers eventually agree on who the next leader is. (:dark_sunglasses: This is a problem with its own Wikipedia page and a long history of solutions based on various constraints!).

## Algorithm: ring election

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](https://en.wikipedia.org/wiki/Leader_election), 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.

:::info
:star: The original ring election papers specify this in slightly different ways, as you may have seen if you've taken Distributed Computing.

For example, the [Chang & Roberts 1979 paper](https://dl.acm.org/doi/10.1145/359104.359108) 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 either version, as long as it meets the two properties below!
:::

:::success
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.
- For simplicity, you can consider the election "won" once every server has the same notion of "highest id in the network".
- **Extra credit**: For +5 extra credit, you can explicitly model a final step of the algorithm where servers send a confirmation of the election being won.

**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-3 paragraphs.
:::

:::info
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.
:::

</details>

# 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.

:::success

### 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:
1. A `check` statement that shows that Alice's buggy algorithm can fail to produce a correct topological sort.
2. 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](http://alloytools.org/quickguide/seq.html); 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).

:::success
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

:::success
In your README, also report:
**Written Q4:** Collaborators?
**Written Q5:** Roughly how long did this assignment take you (in hours)?
:::

This assignment is worth 100 points, broken down by:

:::info
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

*(+5 extra credit: model election win confirmation)*
:::

# 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](http://mitpress.mit.edu/books/software-abstractions) book and a previous version of a [Forge Model Checking](https://docs.google.com/document/u/2/d/e/2PACX-1vQggXOEX__YRulZMhzTSDxpYTp-qLPt6T4Tkj1mZBuQVZJmWjX3An8Q9h23J37_pYajssupeT4M8toQ/pub) assignment from [Tim Nelson's][tim] [Logic for Systems][lfs] at Brown University. Task 2 and 3 are also adapted from Logic for Systems.

[tim]: https://cs.brown.edu/~tbn/
[lfs]: https://csci1710.github.io/2023/