RefinedC merge requestshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests2021-01-28T09:22:29Zhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/17Fix cast insertion in the front end.2021-01-28T09:22:29ZRodolphe LepigreFix cast insertion in the front end.I'll merge this straight away if CI succeeds.
The point of this change is to always use Cerberus to decide what casts to insert on arithmetic operations.I'll merge this straight away if CI succeeds.
The point of this change is to always use Cerberus to decide what casts to insert on arithmetic operations.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/53Generalisation of pointer fragments.2021-04-08T09:46:45ZRodolphe LepigreGeneralisation of pointer fragments.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/54Generalisation of pointer fragments.2021-04-08T13:52:39ZRodolphe LepigreGeneralisation of pointer fragments.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/61Add support for the comma operator.2021-05-19T10:22:57ZRodolphe LepigreAdd support for the comma operator.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/71More provenance2021-06-16T11:13:21ZMichael SammlerMore provenancehttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/75Change rc_copy_alloc_id to do the cast.2021-06-21T08:09:29ZRodolphe LepigreChange rc_copy_alloc_id to do the cast.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/88WIP: VIP2021-07-15T13:54:51ZMichael SammlerWIP: VIPhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/98WIP: parameterise operators with boolean result by the result integer type2021-07-20T08:34:29ZLennard Gähergaeher@mpi-sws.orgWIP: parameterise operators with boolean result by the result integer typeThis PR parameterises Caesium's operators with a "boolean" result (i.e. the comparison operators as well as the derived && and || operators) by a result integer type (which was hard-coded before to i32) as a step to use Caesium for model...This PR parameterises Caesium's operators with a "boolean" result (i.e. the comparison operators as well as the derived && and || operators) by a result integer type (which was hard-coded before to i32) as a step to use Caesium for modelling other C-like languages with different modelling of boolean results (e.g. Rust, which uses single-byte booleans).
Concretely, the changes can be summarised as:
* add a parameter `rit` to the affected operators and use that for the operational semantics of these operators, replacing the `i32` used before.
* adapt the existing notations for these operators to reflect this.
* add new derived notations in `lang/c_notations.v` that instantiate the operators with `i32` so that the codegen for RefinedC does not need to be changed much, and change the Coq codegen to also import this new file.
* adapt the typing proofs to work for the changed operators instantiated to `i32`. Possibly, it might be desirable to support other result types even for C and to generalize the proofs accordingly, but I'm not sure.
The existing examples in the repo compile with these changes, but I haven't tested more exhaustively yet.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/102Use vm_compute in compute_map_lookup2021-07-30T08:26:40ZMichael SammlerUse vm_compute in compute_map_lookuphttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/42Draft: Case study: page table2021-08-19T11:50:13ZFengmin ZhuDraft: Case study: page tableCase study: page tableCase study: page tablehttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/65Remove the layout argument of [free_block].2021-09-20T09:28:04ZRodolphe LepigreRemove the layout argument of [free_block].This information is already contained in the allocation map. Removing
makes it easier to relate to the Cerberus memory model interface.This information is already contained in the allocation map. Removing
makes it easier to relate to the Cerberus memory model interface.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/59Learn side-conditions in the continuation.2021-09-20T09:29:06ZRodolphe LepigreLearn side-conditions in the continuation.This seems to cause some performance penalty. Not sure how significant.This seems to cause some performance penalty. Not sure how significant.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/132Draft: Example scheduler2022-03-15T15:03:16ZMichael SammlerDraft: Example schedulerhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/134add and verify simpler bitmap implementation2022-05-02T09:32:31ZKimaya Bedarkaradd and verify simpler bitmap implementationThis MR introduces the file `priority_modified.h`. This file
contains an alternate implementation of the bitmap that only
supports 64 priorities and is therefore easier to verify. This alternate
implementation of bitmap is fully verified.This MR introduces the file `priority_modified.h`. This file
contains an alternate implementation of the bitmap that only
supports 64 priorities and is therefore easier to verify. This alternate
implementation of bitmap is fully verified.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/137update Iris for later credits2022-07-08T21:43:16ZRalf Jungjung@mpi-sws.orgupdate Iris for later creditsShould help with the nightly build failures. Unfortunately I cannot easily test this locally since the project does not seem to work with ProofGeneral out-of-the-box
```
Error: Cannot find a physical path bound to logical path type with ...Should help with the nightly build failures. Unfortunately I cannot easily test this locally since the project does not seem to work with ProofGeneral out-of-the-box
```
Error: Cannot find a physical path bound to logical path type with prefix refinedc.typing.
```
Note sure what that is about. I see some `_build` things in `_CoqProject`. Maybe dune stuff? Anyway something that breaks the workflow I have been using for 10 years... so let's just see what CI says. ;)
(`make builddep` insists on installing cerberus which I don't want to do since I just want to change some Coq files.)Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/144Verification of bitmap with 256 priorities2023-04-20T13:05:12ZKimaya BedarkarVerification of bitmap with 256 priorities- Delete the old bitmap library supporting 64 priorities.
- Add and use new bitmap library supporting 256 priorities.- Delete the old bitmap library supporting 64 priorities.
- Add and use new bitmap library supporting 256 priorities.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/146Draft: Verification of enqueue and dequeue functions2023-04-21T09:34:32ZKimaya BedarkarDraft: Verification of enqueue and dequeue functionshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/151Verify scheduler data structure2023-06-21T01:04:45ZKimaya BedarkarVerify scheduler data structure- The refinement type for message is also changed to use the ID which is generated from the arrival sequence.
- Verify two functions in the scheduler.h file that enqueue and dequeue messages.- The refinement type for message is also changed to use the ID which is generated from the arrival sequence.
- Verify two functions in the scheduler.h file that enqueue and dequeue messages.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/170Draft: Add specs for some more functions2024-02-02T15:10:45ZKimaya BedarkarDraft: Add specs for some more functions