Open vkuncak opened 9 months ago
The idea would be to use similar injection of assumptions on well-typedness of heap as used in full-imperative
.
Instead of using Array
, we could use a list of pairs for the heap.
The idea is that SharedCell
is not special in stainless. The shared cell as data is indeed only a wrapper for some integer data type (unbounded if want to postpone reasoning about heap overflow).
The key is that it's the update and apply of the ref cell that refer to a global mutable object.
The beauty is that this can be made to work with the existing non-shared memory model. The cells themselves are not shared, it's just that some of them may store identical integers.
The actual implementation for the execution purposes in normal scala should be @inline
method that updates a normal var
inner field of the class.
Maybe something like this would be a sketch of the model we want, if we additionally relax @extern var T
to be ignored for the purpose of alias analysis in case class parameters.
import stainless.annotation.*
import stainless.collection.*
import stainless.lang.*
object SharedListHeap:
type REF = BigInt
case class Heap[@mutable T](var content: Array[T], nextRef: REF):
@extern
def NEW(v: T): SharedCell[T] = ???
@pure
def apply(ref: REF): T = ???
def update(ref: REF, v: T): Unit = {
(??? : Unit)
}.ensuring(_ => apply(ref) == v)
end Heap
given HEAP[@mutable T]: Heap[T] = ???
@extern
class SharedCell[@mutable T](val ref: REF, @extern var content: T):
def apply()(using heap: Heap[T]): T =
heap(ref)
@extern
def update(newValue: T)(using heap: Heap[T]): Unit =
heap.update(ref, newValue)
end SharedCell
case class M(var x:Int)
case class Two(c1: SharedCell[M], c2: SharedCell[M])
def test =
val c = HEAP.NEW(M(32))
val sc1 = c
val sc2 = c
val t = Two(c, c)
()
end SharedListHeap