Add initial pass at iterated views (no checking, restricted format) - Githubissues

septract / starling-tool

An automatic verifier for concurrent algorithms.

MIT License

7 stars 4 forks source link

Add initial pass at iterated views (no checking, restricted format) #64

Closed MattWindsor91 closed 7 years ago

MattWindsor91 commented 7 years ago

Since the working copy for this has ended up tangled up in refactors, here is how iterated views looked when Ben and I finished with them. I'm pushing this to PR now because once I add down closures I imagine the resulting PR would be ridiculously large.

Some things to note:

There is no down closure checking yet. I'll add this next.
Views must be marked as iterated.
We have some working examples (ARC and single-writer multi-reader) but no idea whether their working-ness is correct or a soundness bug.

MattWindsor91 commented 7 years ago

Eep, I left some unit tests dangling. I'll see if I can fix these next week.