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/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 al...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/22Add erasure2019-06-26T12:06:34ZAmin TimanyAdd erasurehttps://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/23generalized rdcss to arbitrary (unboxed) values2019-07-04T08:17:18ZGhost Usergeneralized rdcss to arbitrary (unboxed) valuesFor the expected value at the A location we require that it is unboxed and for the expected value n1 at the B location we require that [InjLV n1] is unboxed.
[new_rdcss] now takes an initial value as argument.For the expected value at the A location we require that it is unboxed and for the expected value n1 at the B location we require that [InjLV n1] is unboxed.
[new_rdcss] now takes an initial value as argument.https://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/24Changed ghost location from location to prophecy variable2019-07-08T17:22:44ZGhost UserChanged ghost location from location to prophecy variableThis change allows using the prophecy erasure theorem to argue that the ghost location does not change the meaning of the original program.This change allows using the prophecy erasure theorem to argue that the ghost location does not change the meaning of the original program.