-
Notifications
You must be signed in to change notification settings - Fork 49
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Reconcile full-imperative using a ShareCell abstraction #1458
Comments
The idea would be to use similar injection of assumptions on well-typedness of heap as used in The idea is that 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 |
Maybe something like this would be a sketch of the model we want, if we additionally relax 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 |
The text was updated successfully, but these errors were encountered: