- If porting CQS to Hazel proves too difficult, add effects to Heaplang.
[x] The problem is that CQS uses logical atomicity which I would also need to port to Hazel first. [x] That combined with having to add proper support for the iInv tactic (i.e. lots of engineering which is technically uninteresting but crucial) might actually make it easier to just add effects to Heaplang. - Alternatively, we could try to prove a lemma that allows us to transport a WP from heaplang to an EWP with the empty protocol.
- Can we use Iris' meta_token for promise_state_done γ
- Use the PR for better effect handling syntax in OCaml to check the examples I give in the thesis.
- try out completely changing tlv dict
- remove future tense where it is unnecessary
- rename logical state to just ghost state.
- Cleanup CQS_Outer_Atomic
- Cleanup Module hierarchy.
- Cleanup Cell_States
- Fix some parts of the hoare style proofs that are hard to understand.
- Add a section on the deferred queue.
- Capitalize figure captions consistently.
- Actually prove the case study.
- Cleanup duplicate info from section 2 (I explain the tryUnregister operation 3 times...)
- Fix that I call it the "Hazel language", it should be the "HH language" and the "Hazel formalism".
- Mostly replace quotation marks by italics
- fix all grammatical errors shown by spellcheck
- Port deferred queue to eio by copying the new dfrac saved_prop implementation to my older Iris version.
- fix missing argument of gspwaiting/gspdone
- fix missing argument of proto/gsiswaker/etc.
- make scheduler result non-optional
- Move repo to mpi gitlab and then place link in pdf
- Add missing citations
- clean up the code, especially
- the case study
- adapted cqs proofs (there are like 20 TODOs in the code)
- Organize the different Iris versions that I am using.