Comments (3)
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.
from stainless.
The actual implementation for the execution purposes in normal scala should be @inline
method that updates a normal var
inner field of the class.
from stainless.
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
from stainless.
Related Issues (20)
- Support for CVC5 HOT 1
- Slowness of `ValueClasses` HOT 1
- Refinement type not properly freshened
- Unsoundness of `no-inc:z3` involving class invariants
- Invalid conterexample in ScanLeft HOT 2
- CVC4/5 unsupported feature shows an error even though another solver is verifying the VC
- IArray support HOT 1
- Size of type parameters
- Incorrect ADT member type approximation HOT 2
- Collection types in Stainless should be inductive
- error: Lookup failed for adt with symbol `Conc$27` in phase FunctionSpecialization HOT 1
- Incorrect "refinements checks for subtyping" generated in some cases
- Deep structure updates in non-aliased imperative (was: `computes` to use condition as a more efficient implementation) HOT 4
- Failure of postcondition shown as failure of the assertion in the branch
- Crash in Inox type checker when using freshCopy HOT 1
- Inline functions that do mutation rejected as ghost HOT 3
- Inconsistent positions for postcondition HOT 1
- Equalities to be rejected: Double, functions, allocatable non-case classes, type vars HOT 4
- `AntiAliasing` not updating targets for `val` fields HOT 2
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from stainless.