Modeling 4: Memory Management
------

# Learning outcomes

:::info
In this assignment, you will:
- Continue practicing using temporal logic operators to model a system.
- Wrangle with the details of one automatic memory management strategy: reference counting.
- Use Alloy to show that one desirable system property *does not hold*.
- Practice reasoning about soundness and completeness.
:::

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.

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

:::success
:star: This assignment is based on a stencil file, which you can [download here](https://drive.google.com/file/d/1W8Zh_-_3_pr3hVJsiLWP9wrxkTzF3U0i/view?usp=sharing).
:::

## 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/)

# Assignment description

In this assignment, you will use Alloy's temporal logic to finish the **reference counting** model that we started in class.

Using the [stencil file](https://drive.google.com/file/d/1W8Zh_-_3_pr3hVJsiLWP9wrxkTzF3U0i/view?usp=sharing) is required for this assignment.

:::info
The stencil file is essentially the basic model we started together in class, plus (1) a completed `validTraces` predicates, (2) structure for you to handle "cascades" (see below), and (3) more empty predicates for you to fill in.
:::

:::info
:star: **Remember to turn Overflow off (Search > Overflow) for this model.
:::

## Workshop: Helper predicates

In workshop, we'll start by implementing the following 3 helper predicates, all of which are for a single state in time:

------------------------- Helper predicates -----------------------------

// Takes the var fields as arguments, so we can use this pred "now" and "after"
pred reachableFromRootSet[o: HeapObject, refs: Memory->HeapObject] {

}

// Soundness: memory safety: no reachable memory has been freed.
pred memorySafe[alloc: Allocated, refs: Memory->HeapObject] {

  // Everything reachable from the root set is still allocated (not free)

}

// Completeness: no leaks in the given step (we've freed everything that is
// no longer reachable).
pred noLeaks[alloc: Allocated, refs: Memory->HeapObject] {

  // Everything we have not freed is actually reachable. No leaked, no longer
  // reachable memory.
}

## Task 0: Background reading

:::success
**README**

*Start a `README` and answer the following written questions there:*

Read sections 1-2.1 and section 2.6 of [Uniprocessor Garbage Collection Techniques](https://courses.cs.washington.edu/courses/cse590p/12wi/wilson_gc.pdf).

**Written Q1:** Explain in one paragraph, in your own words, what the paper means by "transitive decrementing of reference counts".

**Written Q2:** Explain in one paragraph, in your own words, what the paper means by "conservative" garbage collection. Why can't systems use non-conservative garbage collection for C/C++ programs?
:::

## Task 1: Modeling changes over time

Your first task is to fill in predicates that describe changes over time.

In each predicate, reuse existing predicates as much as possible.

:::success

**Init**

Fill in `init`. Constrain the model to initially have no memory safety issues or leaks (invoke the existing predicates).

Additionally, constrain the model such that everything in the heap is initially reachable from the root set.
:::

:::success

**Modeling the programmer making changes**

Fill in `heapChangedByProgrammer`.

In this step, we want to model:
1. New objects being allocated. The `Memory` sig itself is not variable, but the `Allocated` sig is. Note that the set of `Allocated` objects should never shrink in this step, because the programmer never calls `free` explicitly in reference counting.
2. Keep in mind that the programmer cannot create references to unallocated memory, so in this step, if an object is reachable from the root set, it should be allocated.
:::

#### Reference counting "cascades"
For reference counting itself, we will break it down into two steps, one of which is completed for you.

In an automatic references counting system, one step is to free any heap object whose reference count hits zero. This is what you will implement.

The next step is to "cascade": any freed object could have outgoing references, and those references must be removed. Once those references are removed, the first step may need to be repeated (which can loop). The stencil file has logic to cascade implemented for you as a fact; you just need to fill in the first step.

:::success
**Reference counting**

Fill in `referenceCountingFrees`.

In this step, no references should change, but the set of allocated objects should change. Use existing predicates as much as possible.

Model what should happen when a heap object's reference count reaches 0.

**README**

**Written Q3:** Write a snippet of code that shows why a reference counter needs to cascade, even if there are no cycles in the reference graph. That is, construct an example where just freeing an object whose reference count is 0 does not free all objects that should be freed. Include a short explanation or diagram.
:::

:::success
**Do nothing**

Fill in `doNothing`, following the pattern we have seen before.
:::

The stencil has one predicate and run, `someCascade`, to test instances once you fill in `referenceCountingFrees`. However, you may want to write more of your own predicates and run statements (taking inspiration from the last assignment). These will not specifically be graded, but may help you design a better model.

## Task 2: Verifying soundness and completeness

Next, you'll fill in predicates to check the soundness and completeness of reference counting.

:::success
**Soundness**: fill in `soundness`. See the lecture notes for the definition we want here. The desired property should hold in every step; use existing predicate(s) where possible.

**Completeness**: fill in `completeness`. For the purposes of this assignment, we will define completeness as this: since the cascade logic may take an unknown number of steps after `referenceCountingFrees` is run, we will just require that eventually there are no memory leaks.

**Written Q4:** Do you expect soundness to hold for reference counting? Why or why not? Does your Alloy check increase your confidence? If you find a counterexample, explain it here.

**Written Q5:** Do you expect completeness to hold for reference counting? Why or why not? Does your Alloy check increase your confidence? If you find a counterexample, explain it here.
:::

## [Independent] Task 3: Modified reference graph

<details>
<summary>Only start on this task after you have completed the previous tasks! Click to expand. </summary>
<br>

:::success
**[Independent]** Add in a new predicate that restricts the reference graph such that reference counting is complete based on the definition for this assignment. Think of this as defining a subset of memory-altering programs for which reference counting *is* complete. Fill in completenessWithRestrictedReferenceGraph and show that if this property is true, reference counting becomes complete.

**Written Q6:** Would it be practical to have an automated memory management system rely on this predicate/assumption? Why or why not?
:::

</details>
<br>

## [Optional, extra credit] Task 4: Reference counting and cycles in Rust

<details>
<summary>Only start on this task after you have completed the rest of the assignment! Click to expand. </summary>
<br>

:::success
Read sections 4-4.2 and then section 15.6 of [this version of the Rust Book](https://rust-book.cs.brown.edu/ch15-06-reference-cycles.html). Complete the quiz questions included as part of the book.

**Written EC**: Explain in a few paragraphs, in your own words, how weak references can help prevent memory leaks due to cycles in the reference graph. Can a weak reference be used in the same way as a standard reference? How do they differ?
:::

</details>
<br>

# Grading

:::success
In your README, also report:
**Written Q7:** Collaborators other than your partner?
**Written Q8:** Roughly how long did this assignment take you (in hours)?
:::

This assignment is worth 100 points, broken down by:

:::info
40 points: State change predicates
- 5: `init`
- 15: `heapChangedByProgrammer`
- 15: `referenceCountingFrees`
- 5: `doNothing`

35 points: Predicates to verify soundness and completeness
- 10: `soundness`
- 15: `completeness`
- 10: `completenessWithRestrictedReferenceGraph`

25 points: `README`/**Written Qs** 1-8

(_Up to +10 extra credit for Task 4_)
:::

# Submission
Submit the following 2 files on Gradescope: `ref_counting.als` and `README.{txt, md}`.

# Attribution
This exercise is adapted from on a previous version of a [Forge Model Checking](https://docs.google.com/document/u/2/d/e/2PACX-1vQo6ctFWibVmsgME5zHF_lH3T1w8vGtcarTQHntoerscwll4t6k8k0RhE96mS2SDC8ipbCXjdFn2ms5/pub) assignment from [Tim Nelson's][tim] [Logic for Systems][lfs] at Brown University.

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