This lab requires you to run AmalgamExperimental, a modified version of Alloy. Amalgam behaves exactly like Alloy, except some minor usage data is logged locally, and the underlying solver has been altered to display different Alloy instances first. Providing research data is opt-in, and you do not have submit responses or your log to the survey at the end of this lab.
To run AmalgamExperimental (not AmalgamBeta), open a terminal, type amalgamlab, and press Enter. If you have issues running the command, please ask for assistance.
In this lab, we'll model memory as a collection of Memory cells:
abstract sig Memory {}
Memory is marked as abstract because a cell may either be a HeapCell:
sig HeapCell extends Memory {}
...or appear on the Stack:
one sig Stack extends Memory {}
While there may be many discontiguous regions of allocated heap memory, there is only one contiguous range of allocated stack memory. The Stack memory is the starting point from which a program may traverse references to reach other parts of memory.
So far, the model lacks a notion that memory cells may have references to other memory cells. For some applications, it might be suitable to simply add a references field to Memory:
abstract sig Memory {
references: Memory
}
references: Memory to references: HeapCell?
In this lab, we will be considering a type of automatic memory management—systems that automatically manage the deallocation of memory as references between memory cells change. To reflect that the references of any given memory cell may change over time, we need to move references out of Memory and into a new signature representing the memory state at a particular time:
abstract sig State {
references : ...
}
For this problem, we will only consider two states (StateA and StateC), plus an intermediate state (StateB):
one sig StateA, StateB, StateC extends State {}
references field from the Memory signature. Add the State, StateA and StateC signature to your model. Replace the ellipsis with the appropriate type.
At first, it may appear that this change has mostly had the effect of making the visualization of the model far more tangled. We would like to easily see what has changed between states. To do this, we can project over the State signature using the drop-down Projection menu on the toolbar of the visualizer.
State signature. Use the arrows at the bar on the bottom of the visualization screen to switch the projection between StateA and StateB. If the visualization graph does not contain any edges, click Next until you are viewing a model which does have references.
Automatic memory management systems keep track of which heap memory cells are allocated and which are not at each state. We can capture this by adding an allocated member to the State signature:
abstract sig State {
allocated : ...,
references : ...,
}
allocated field to the State signature in your model. Replace the ellipsis with the appropriate type.
Memory management systems are evaluated, in part, by the degree to which they don't deallocate memory too early (soundness), and the degree to which they don't deallocate memory too late (completeness). Recall that the Stack memory is the starting point from which a program may traverse references to reach other parts of memory. So, if memory is still reachable from the program Stack, we're still using it. We hope that our memory management system keeps everything we are using is still allocated (soundness), and tosses everything we are not longer using (completeness).
pred reachFromStack[m : HeapCell, state : State] {
...
}
reachFromStack, which should be true only when the HeapCell memory can be reached starting at the Stack memory in the given State.
The Stack memory is the starting point from which a program may traverse references to reach other parts of memory. A memory state is safe if all memory reachable from the Stack is allocated:
pred safe[state : State] {
...
}
A memory management system is sound if acting on an initial safe memory state implies that the following state will also be safe:
check soundness {
safe[StateA] => safe[StateC]
} for 4 Memory
safe. Since you have not described exactly how the memory manager will transition between StateA and StateC, expect that this assertion check will fail.
A memory state is clean if all allocated memory is reachable from the Stack:
pred clean[state : State] {
...
}
A memory management system is complete if acting on an initial clean memory state implies that the following state will also be totally collected:
check completeness {
clean[StateA] => clean[StateC]
} for 4 Memory
clean. Since you have not described exactly how the memory manager will transition between StateA and StateC, expect that this assertion check will fail.
Reference counting is a form of automatic memory management. For each cell of heap memory, a reference counting collector stores the number incoming references to it. When a memory cell's reference count drops to zero, the cell is unallocated.
To represent this, will write a function ref_count that returns the number of incoming references to a HeapCell in a certain State:
fun ref_count[state: State, cell: HeapCell]: Int {
...
}
ref_count correctly computes the number of incoming references for a cell in a given state.
Between StateA and StateB, the program may create or destroy references:
fact A_to_B_AllocatedUnchanged {
...
}
A_to_B_AllocatedUnchanged to your model, and complete the implementation such that the set of allocated memory cells do not change between StateA and StateB
StateB and StateC, references should not change. The set of allocated may change as a result of garbage collection. A reference counting collector will enforce that for all memory cells, a cell will not be allocated in StateC iff it has a reference-count of 0 in StateB.
fact B_to_C_GarbageCollected {
...
}
B_to_C_GarbageCollected to your model, and complete the implementation such that the set of references between memory cells do not change between StateB and StateC, and the set of allocated memory cells changes appropriately.
soundness and completeness assertions. Is reference-counting collection sound or complete? If not, why? How do the consequences of violating soundness compare the consequences of violating completeness?
If you implemented reference counting correctly, soundness should not be violated. If you are getting counterexamples, try fixing the problem yourself, or ask a TA for help.
Unless you wrote some extra constraints, completeness should be violated. If you are not getting counterexamples, try fixing the problem yourself, or ask a TA for help. There are many reasons why our current reference counting implementation is not complete. Let's fix two of those now by adding the following facts:
fact UnallocatedCantReference {
all s : State | all m : HeapCell - s.allocated | no s.references[m]
}
However, our implementation is still not complete!
completeness assertion, and explore the models Amalgam returns. Do you know what the problem is? Do you know how to fix it?