MemoryTracking.tla

--------------------------- MODULE MemoryTracking ---------------------------
(* A memory allocator which tracks usage by "phase" *)

CONSTANTS Phase, (* A set of phases *)
          Thread, (* A set of threads *)
          Address (* A set of addresses *)
          
VARIABLES memory, (* All in-use allocations *)
          memoryByPhase, (* A mapping from phases to sets of allocated items *)
          memoryByThread (* A mapping from threads to an allocated record *)         
          
-----------------------------------------------------------------------------

States == { "alloc", "free", "none" }

MemoryAllocation == [ addr : Address, phase: Phase, state : States ]

DontCareAddress == CHOOSE a \in Address : TRUE
DontCarePhase == CHOOSE p \in Phase: TRUE
 
(* TLC gives no help if you screw up and use ":" here instead,
   complains about not being able to enumerate the rhs of each assignment *)
NoAllocation == [ addr |-> DontCareAddress, phase |-> DontCarePhase, state |-> "none" ]
 
Init ==
  /\ memory = {}
  /\ memoryByPhase = [ p \in Phase |-> {} ]
  /\ memoryByThread = [ t \in Thread |-> NoAllocation ]
              
TypeInvariant == 
  /\ memory \in SUBSET MemoryAllocation
  /\ memoryByPhase \in [Phase -> SUBSET MemoryAllocation] (* Each phase has a list, but order not important *) 
  /\ memoryByThread \in [Thread -> MemoryAllocation] (* Each thread can only be doing one allocation or deallocation at a time *)

(* Newly assigned addresses must not already be in use, even by any thread 
   which just allocated it *)
AddressNotInUse(m1) ==
  /\ ~\E m2 \in MemoryAllocation : m2 \in memory /\ m1.addr = m2.addr  
  /\ ~\E t \in Thread : m1.addr = memoryByThread[t].addr
  
(* Non-critical section: allocate some memory from the heap *)       
AllocNoncritical(t,p) == 
  /\ memoryByThread[t].state = "none"
  /\ \E m \in MemoryAllocation :
        /\ m.state = "alloc"
        /\ m.phase = p
        /\ AddressNotInUse(m)  
        /\ memoryByThread' = [ memoryByThread EXCEPT ![t] = m ]
  /\ UNCHANGED <<memoryByPhase, memory>>
        
(* Critical section; add it to the list for the phase it was allocated (and return it for use.) *)        
AllocCritical(t) == 
  LET m == memoryByThread[t] IN
    /\ m.state = "alloc"
    /\ memoryByPhase' = [ memoryByPhase EXCEPT ![m.phase] = memoryByPhase[m.phase] \union { m } ]
    /\ memoryByThread' = [ memoryByThread EXCEPT ![t] = NoAllocation ]
    /\ memory' = memory \union { m }
    
(* Non-critical section: mark the memory free (this is the bug) *)
FreeNoncritical(t,m) ==
  LET m2 == [ addr |-> m.addr, state |-> "free", phase |-> m.phase ] IN
    /\ m \in memory
    /\ memoryByThread[t].state = "none"
    /\ memoryByThread' = [memoryByThread EXCEPT ![t] = m2]
    /\ memoryByPhase' = [memoryByPhase EXCEPT ![m.phase] = (memoryByPhase[m.phase] \ {m}) \union {m2} ]
    /\ memory' = (memory \ { m }) \union { m2 } 
    
(* Critical section: remove the memory from the phase list *)
FreeCritical(t) ==
  LET m == memoryByThread[t] IN
    /\ memoryByPhase' = [memoryByPhase EXCEPT ![m.phase] = memoryByPhase[m.phase] \ {m}]
    /\ memoryByThread' = [memoryByThread EXCEPT ![t] = NoAllocation ]
    /\ memory' = memory \ { m }

(* Enumerating over m \in memoryByPhase[m] didn't work *)
AllAlloced == \A p \in Phase : \A m \in MemoryAllocation : m \in memoryByPhase[p] => m.state = "alloc"
      
----------------------------------------------------------------------------

Next == 
 \/ \E t \in Thread, p \in Phase : AllocNoncritical(t, p)
 \/ \E t \in Thread : AllocCritical(t)
 \/ \E t \in Thread, m \in MemoryAllocation : FreeNoncritical(t, m)
 \/ \E t \in Thread : FreeCritical( t )

vars == <<memory,memoryByPhase,memoryByThread>>
    
Spec == Init /\ [][Next]_vars

AllocPossible == 
  /\ \E t \in Thread, p \in Phase :  ENABLED(AllocNoncritical(t,p))
 
AddressFree == 
  /\ \E m \in MemoryAllocation : AddressNotInUse(m)
  
-----------------------------------------------------------------------------

THEOREM Spec => [] TypeInvariant

THEOREM Spec => [] AllAlloced

=============================================================================