examples merge requestshttps://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests2019-01-25T10:19:51Zhttps://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/1update for more general saved_prop2019-01-25T10:19:51ZRalf Jungjung@mpi-sws.orgupdate for more general saved_propThis is the iris-examples side of https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/76This is the iris-examples side of https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/76https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/2Amin/logrel2019-01-25T10:19:51ZAmin TimanyAmin/logrelAdd logical relations from IPM paper to iris-examples. This closes #2.Add logical relations from IPM paper to iris-examples. This closes #2.https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/3Add the spanning tree algorithm.2019-01-25T10:19:51ZAmin TimanyAdd the spanning tree algorithm.This closes #3.This closes #3.https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/4Make EqType more realistic2019-01-25T10:19:51ZAmin TimanyMake EqType more realisticThis MR makes EqTypes (types on which you can CAS) more realistic. EqTypes are now: unit, boolean natural numbers and references. Having references in EqTypes makes the fine-grained stack example syntactically well-typed.This MR makes EqTypes (types on which you can CAS) more realistic. EqTypes are now: unit, boolean natural numbers and references. Having references in EqTypes makes the fine-grained stack example syntactically well-typed.https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/5Implement modular specifications from the HOCAP paper2018-06-20T15:55:54ZDan FruminImplement modular specifications from the HOCAP paperThis branch formalises the specifications for the concurrent bag and concurrent runners from the paper
[Modular Reasoning about Separation of Concurrent Data Structures](http://www.kasv.dk/articles/hocap.pdf)
Kasper Svendsen, Lars Bir...This branch formalises the specifications for the concurrent bag and concurrent runners from the paper
[Modular Reasoning about Separation of Concurrent Data Structures](http://www.kasv.dk/articles/hocap.pdf)
Kasper Svendsen, Lars Birkedal, Matthew Parkinson.
Might be interesting for iris-examples, otherwise I can put it in a different repository.
TODO list:
- [x] Clean up and document the code
- [x] Explain the differences with the formalisation in the paper
- ~~Monotone bag specification~~ doesn't make much sense actually
- [x] Bag with contributions specification (requires `gmultiset` RA)https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/6Add more examples from the lecture notes.2018-04-24T11:46:27ZAleš Bizjakales@alesb.comAdd more examples from the lecture notes.Adds more of the examples from the iris lecture notes (and some additional ones).Adds more of the examples from the iris lecture notes (and some additional ones).Aleš Bizjakales@alesb.comAleš Bizjakales@alesb.comhttps://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/7Fix a file broken due to wp_binop changes2018-04-30T09:25:08ZDan FruminFix a file broken due to wp_binop changes--https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/8port to gen_proofmode2018-07-13T09:18:19ZRalf Jungjung@mpi-sws.orgport to gen_proofmodeUnfortunately `rewrite` stopped working in a few cases, which I worked around because I did not know how to fix it.
Cc @robbertkrebbersUnfortunately `rewrite` stopped working in a few cases, which I worked around because I did not know how to fix it.
Cc @robbertkrebbershttps://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/9Logically atomic stack2018-07-13T11:17:22ZRalf Jungjung@mpi-sws.orgLogically atomic stackThis relies on https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/163 being merged.This relies on https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/163 being merged.https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/10WIP: fix for stronger CAS requirements2018-07-04T13:55:41ZRalf Jungjung@mpi-sws.orgWIP: fix for stronger CAS requirementsDepends on https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/167
Fixes #7, #8Depends on https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/167
Fixes #7, #8https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/11A new version of concurrent_stack2019-03-04T13:57:16ZDaniel GratzerA new version of concurrent_stackThis pull request contains a new version of the concurrent_stack examples. They compile with the CAS restrictions
as well as the other updates to Iris. The proofs are also more clean for the 3rd and 4th version.
Happy to improve this...This pull request contains a new version of the concurrent_stack examples. They compile with the CAS restrictions
as well as the other updates to Iris. The proofs are also more clean for the 3rd and 4th version.
Happy to improve this further if people have any improvements.
Fixes #8https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/12Semantic typing for heap_lang2019-01-25T10:26:47ZRobbert KrebbersSemantic typing for heap_langIn this MR I define a semantic typing judgment for heap_lang, prove all the usual typing rules, safety, and semantic typing of the symbol table example from @dreyer's POPL talk.
Some interesting differences compared to the current log...In this MR I define a semantic typing judgment for heap_lang, prove all the usual typing rules, safety, and semantic typing of the symbol table example from @dreyer's POPL talk.
Some interesting differences compared to the current logrel development:
### Expressions
- By building on top of heap_lang, we get the nice notations and tactics from heap_lang for free. No more De Bruijn for expressions!
- I only defined semantic types, not syntactic types. One could define syntactic types in the future and prove the fundamental theorem, but I was not too interested in doing that.
- Due to the value restriction, we need to thunk `∀` types. I thus model the type-level abstraction `Λ e` as `λ: <>, e` and the type level application `e _` as `e #()`.
- Due to step-indexing, we need to take a step to prove the typing rule for unfolding recursive types. I defined the unfold operator `rec_unfold e` as `(λ: "x", "x") e`.
### Types
- By having only semantic types, I could use Coq's binders in ∀ and ∃ types, and have nice notations. So, no more De Bruijn for types either.
- I defined a type `lty` as a record containing a predicate over values and a prove that the predicate is persistent. Notably, I used this record in the interpretation of ∀ and ∃ types, and thus no longer have to explicitly require the type to be persistent.
### Typing judgment and typing rules
- I defined the semantic typing judgment `Γ ⊨ e : A` as an `iProp` and stated all of the typing rules using `-∗`.
- I used type classes for operator typing (`LTyUnOp`, `LTyBinOp`) and to keep track of unboxed types (`LTyUnboxed`).
CC @amintimany @dfrumin @dreyerhttps://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/13Master2019-03-06T12:41:15ZDaniel GratzerMasterI messed up git and so I had to make a new request... sorry folks.
This includes the specs and stuff though.I messed up git and so I had to make a new request... sorry folks.
This includes the specs and stuff though.https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/14Add a copy of my new (logically atomic) specification of the Treiber stack algorithm.2019-03-06T16:50:20ZRodolphe LepigreAdd a copy of my new (logically atomic) specification of the Treiber stack algorithm.The example was originally developed here: https://gitlab.mpi-sws.org/lepigre/treiber_stack.The example was originally developed here: https://gitlab.mpi-sws.org/lepigre/treiber_stack.https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/15Fix atomic snapshot example2019-03-28T11:58:59ZRodolphe LepigreFix atomic snapshot exampleUpdate to the new prophecy variable interface (with lists).Update to the new prophecy variable interface (with lists).https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/16Shorter barrier proof that uses auth instead of sts.2019-05-28T06:34:03ZRobbert KrebbersShorter barrier proof that uses auth instead of sts.The title says it all :)The title says it all :)https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/17Bump Iris with changes in `auth`2019-05-24T11:44:21ZHai DangBump Iris with changes in `auth`Title says it all.Title says it all.https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/18Some [positive] was sometimes used for [loc], which is now abstract.2019-05-31T16:56:47ZRodolphe LepigreSome [positive] was sometimes used for [loc], which is now abstract.https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/19Fix and conditional increment example2019-06-04T15:45:49ZRodolphe LepigreFix and conditional increment examplehttps://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/20Branded Types2020-09-29T09:30:11ZSimon SpiesBranded TypesThese two examples use the logical relation of Heaplang to define arrays and vectors.
Arrays are fixed-size and provide safe and unsafe functions to access their elements.
Vectors can grow in size and use the unsafe array methods to ac...These two examples use the logical relation of Heaplang to define arrays and vectors.
Arrays are fixed-size and provide safe and unsafe functions to access their elements.
Vectors can grow in size and use the unsafe array methods to access their elements.
Safety is ensured by branding vectors, meaning each vector is tagged with a
fresh type variable. Statically, this has a similar effect as existential types.
Semantically, the type variable is used to encode an ADT, i.e. impose invariants on the vector.Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.org