A Formal Proof of Absence of Memory Leaks in Argentum Programming Language for the Single-Threaded Case

Definitions and Assumptions

1. Argentum has two kinds of objects:
   1. Single-owner mutable objects
   2. Shared immutable objects.
2. Argentum has five types of pointers:
   1. Temporary pointers: T that protect mutable objects accessible from stack
   2. Owning pointers: @T that hold mutable objects
   3. Weak pointers: &T that reference mutable objects which are upheld somewhere else
   4. Shared pointers: *T that hold immutable objects
   5. WeakToImmutable pointers: &*T that reference immutable objects
3. Pointer limits, that are enforced at compile time:
   1. Temporary pointers can reside only in stack frames as function parameters, temporary values and local variables. They cannot reside in heap - as object fields and array items.
   2. Owning pointers cannot be function parameters.
   3. Reading value of a variable V of type @T returns @T only when it is a return expression of a block or function scope and V is a local variable in this scope. In all other cases V reads as temporary pointer T.
   4. Immutable objects cannot reference mutable objects.
   5. All other pointers can be used with no limitations.
4. Object lifetime conditions:
   1. Mutable objects live as long as they are referenced by at least
      1. one owning reference
      2. or any number of temporary references.
   2. Immutable objects live as long as they are referenced by at least one shared reference.

Statement 1:
In absence of cycles by owning pointers all object life times can be controlled with ref-counting.

Definitions and Assumptions

1. Objects and References:
   • Each object O has a reference count RC(O), which tracks how many owning pointers refer to O.
2. Retain and Release Operations:
   • Retain: Increases the reference count of an object by one.
   • Release: Decreases the reference count of an object by one. If the reference count reaches zero, the object is deallocated.
3. No Cycles with Strong Pointers:
   • There are no cycles of owning pointers, meaning that it is impossible to have a circular chain of references where each object in the chain has a non-zero reference count because of another object in the chain.

Proof

Initialization: When an object O is created, its reference count RC(O) is initialized to one (due to the initial owning pointer created at allocation). RC(O)=1

Retain Operation: Each time an owning pointer to an object O is created (retained), the reference count of O is incremented by one: retain(O)  ⟹  RC(O)=RC(O)+1

Release Operation: Each time an owning pointer to an object O is destroyed (released), the reference count of O is decremented by one: release(O)  ⟹  RC(O)=RC(O)−1

If the reference count RC(O) reaches zero, O is deallocated: RC(O)=0  ⟹  deallocate(O)

Absence of Cycles: Given that there are no cycles of owning pointers, every object O can only be referenced by other objects in a DAG-like structure. Each object ultimately traces back to a root object that is directly referenced by a live variable or the root set of the program (e.g., global variables, stack variables).

Root Set: Consider the root set R containing all objects directly referenced by the program's live variables. These are the entry points for the retain/release mechanism. The reference count for each object in R is managed by the program's live variables.

Memory Deallocation: When the program's execution releases all owning pointers to an object O:

1. Direct Release: If an object is directly released and no other owning pointers reference it, its reference count reaches zero, and it is deallocated.
2. Propagation: If an object O is deallocated, all objects it references with owning pointers will have their reference counts decremented. This decrement can propagate, potentially deallocating other objects whose reference counts reach zero.

Absence of Leaks: Since there are no cycles, the reference count of any object O eventually reaches zero when there are no more owning pointers referencing it. As a result, O will be deallocated. There cannot be a memory leak (unreachable allocated memory) because:

• Every object will eventually have its reference count decremented to zero once it is no longer referenced.
• The absence of cycles ensures there are no reference count increments that maintain a non-zero reference count without any live references from the root set.

Statement 2: Argentum guarantees the absence of cycles by temporary pointers `T`

Proof

1. Stack frames live in CPU stacks and disposed immediately upon function return. CPU stack frames do not form cycles.
2. Temporary references reside in stack frames only (per 3.1).
3. Which guarantees that they do not form cycles too.

Statement 3: Argentum guarantees the absence of cycles by owning pointers `@T`

Proof

Owning pointers can reside in stack frames and object fields. Owning references residing in stack frames do not form cycles as shown in Statement 2. Let’s prove that owning references residing in object fields cannot form cycles as well. Object fields of type @T can be assigned only with expression of type @T. These expressions are:

• New Instance creation expression.
• Results of the @copy operator that creates a new instance.
• Results of a function/method call that returns @T result, that recursively can be only a newly crated object instance.

In the expression O.F := E;
where:

• a field F of an object O is the recipient
• a result V (of type @T) of the expression E is assignee

The object O and its field F preexist V, and as such F never resides in the object V and in any of objects inside subtree of V. This guarantees absence of circular references in the hierarchy of owning @T pointers.

Assumptions 3.2 and 3.3 prevent creation of assignee V prior to the recipient O by passing V as a parameter or reading it from variables.

Statement 4: Argentum guarantees the absence of cycles by shared pointers `*T`

Proof

Shared object O lives as long as  it referenced by at least one *T shared reference. Shared references can reside in stack frames (where, as proven in the Statement2, they don’t form cycles) and in object fields. In Argentum, shared objects are strictly immutable (Assumption 1.2). Immutable objects cannot reference mutable objects (Assumption 3.3), thus all immutable subtrees cannot be modified under any circumstances. This rule prevents cycles in Shared references:

• In order to form a cycle we need to assign
  • a shared reference to an object A
  • to the field of the object B,
  • such as A is B or A has already had a shared reference to B.
• If A has a shared reference to B this means B is immutable (as a target of the shared reference) and as such its field cannot be assigned.
• If A is B, we first need to acquire a Shared reference to it, and for that we need to make object A immutable, which makes it impossible to assign anything to its fields in the next step.

Thus shared references cannot create graph topologies having cycles. They always form directed acyclic graphs, and as such they are leak-free.

Statement 5: Weak pointers &T and &*T cannot leak objects

Weak references can form loops in object topology, but they do not control target object lifetimes. Prior to use they must be locked and checked for target object existence. Locking of a weak pointer &T produces a Temporary (stack-only) pointer T, not shared *T or owning @T pointers (as C++, Rust, Swift etc. do). Since we proved in the Statement 2 that Temp references are leak-free, Weak references are also leak-free.

Weak-to-immutable is a special form of weak reference to immutable shared object that, when locked, produce shared reference. Since it references immutable objects, it cannot be assigned inside the hierarchy to which it points to, and as such it never produces loops in pointer topologies and never leaks memory.

This concludes the formal proof of leak-free data structures of Argentum programming language in a single-threaded case.

See also: multi-threaded case.