Modeling 4: Reference Counting

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.

Setup

You can run this assignment locally, on your own machine. This assignment uses Alloy 6, as installed in the previous assignments.

:star: This assignment is based on a stencil file, which you can download here.

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

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 is required for this assignment.

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.

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

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.

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.

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.

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

Start a README and answer the following written questions there:

Written Q1: 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.

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.

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 referenceCountingFree is run, we will just require that eventually there are no memory leaks. That it, in every step it should be true that if the current step is referenceCountingFree, then eventually we expect there to be no memory leaks.

Written Q2: 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 Q3: 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

Only start on this task after you have completed the previous written questions! Click to expand.

[Independent] Add in a new predicate that restricts the reference graph such that reference counting is complete based on the definition for this assignment. Fill in completenessWithRestrictedReferenceGraph and show that if this property is true, reference counting becomes complete.

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


Grading

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

This assignment is worth 100 points, broken down by:

40 points: State change predicates

40 points: Predicates to verify soundness and completeness

20 points: README/Written Qs 1-6

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 assignment from Tim Nelson's Logic for Systems at Brown University.