RefinedC merge requestshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests2022-09-13T15:24:26Zhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/141Port to 8.16.02022-09-13T15:24:26ZMichael SammlerPort to 8.16.0https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/142Fix W.subst_l slowdown2023-03-07T11:38:55ZLennard Gähergaeher@mpi-sws.orgFix W.subst_l slowdownThis fixes a slowdown where the time `simpl` takes to simplify `W.subst_l` blows up exponentially with the number of local variables.
(In RefinedRust, the current definition therefore makes it intractable to verify functions with 30+ loc...This fixes a slowdown where the time `simpl` takes to simplify `W.subst_l` blows up exponentially with the number of local variables.
(In RefinedRust, the current definition therefore makes it intractable to verify functions with 30+ local variables).
In my tests, the new definition has performed measurably better once more than 19-20 variables are involved, while performing similarly on fewer variables.
Thus, there is no measurable advantage for the current RefinedC case studies, but in case someone ever verifies a function with lots of local variables, this might still be useful.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/143add note in developers.md for mlgmpidl library and small corrections in the a...2023-04-04T09:06:37ZKimaya Bedarkaradd note in developers.md for mlgmpidl library and small corrections in the annotations docshttps://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/145add bitmap with 256 priorities2023-06-16T16:47:48ZKimaya Bedarkaradd bitmap with 256 priorities- Fix small errors in Coqproject and Makefile for scheduler
- Delete bitmap with 64 priorities
- Add bitmap with 256 priorities- Fix small errors in Coqproject and Makefile for scheduler
- Delete bitmap with 64 priorities
- Add bitmap with 256 prioritieshttps://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/147use primitive projections for iProp_to_Prop2023-05-14T09:15:35ZMichael Sammleruse primitive projections for iProp_to_PropSmall performance win: https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=refinedc&var-branch1=master&var-commit1=a09a919f04f114de27a324641b36edbdd5242ed0&var-config1=build-coq.8.17.0-timing&var-branch2=time%2FiPro...Small performance win: https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=refinedc&var-branch1=master&var-commit1=a09a919f04f114de27a324641b36edbdd5242ed0&var-config1=build-coq.8.17.0-timing&var-branch2=time%2FiProp_to_Prop_primitive_proj&var-commit2=f43db09c385c0212f59c894e694ae730dea86ac3&var-config2=build-coq.8.17.0-timing&var-metric=instructions&var-group=(.*)https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/148Unbundle rtype to make more things typeclasses opaque2023-05-30T14:56:53ZMichael SammlerUnbundle rtype to make more things typeclasses opaqueGives a around 5% performance win: https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&var-metric=instructions&var-project=refinedc&var-branch=All&var-config=All&var-group=%28%29.%2A&from=1684544604618&to=1685458516969Gives a around 5% performance win: https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&var-metric=instructions&var-project=refinedc&var-branch=All&var-config=All&var-group=%28%29.%2A&from=1684544604618&to=1685458516969https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/149Refactor the Lithium files2023-05-31T09:41:17ZMichael SammlerRefactor the Lithium fileshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/150Refactor Lithium2023-06-01T16:36:45ZMichael SammlerRefactor Lithiumhttps://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/152remove specialized typeclasses2023-06-05T13:53:48ZMichael Sammlerremove specialized typeclasseshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/153Automatically generate typeclass instances2023-06-06T13:06:44ZMichael SammlerAutomatically generate typeclass instanceshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/154simpler definition of simplify_goal2023-06-07T10:21:16ZMichael Sammlersimpler definition of simplify_goalhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/155Cleanup new Lithium Syntax2023-06-13T11:00:05ZMichael SammlerCleanup new Lithium Syntaxhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/156add scheduler data structure2023-06-27T11:35:40ZKimaya Bedarkaradd scheduler data structure- Changes to the message queue library to make verification of scheduler data structure possible
- Verifying the enqueue and dequeu operations of the scheduler data structure- Changes to the message queue library to make verification of scheduler data structure possible
- Verifying the enqueue and dequeu operations of the scheduler data structureKimaya BedarkarKimaya Bedarkarhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/157Verify fds data structure functions2023-07-19T06:24:25ZKimaya BedarkarVerify fds data structure functionshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/158Remove continuation from SimplAnd and SimplImpl2023-07-25T14:32:26ZMichael SammlerRemove continuation from SimplAnd and SimplImplhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/159Keep sideconditions inside the iris ctx2023-07-25T15:50:10ZMichael SammlerKeep sideconditions inside the iris ctxThis is in preparation to keep existential quantifiers in the goal. It has even a small benefit for performance: https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=refinedc&var-branch1=master&var-commit1=f3820ba52a...This is in preparation to keep existential quantifiers in the goal. It has even a small benefit for performance: https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=refinedc&var-branch1=master&var-commit1=f3820ba52a435b7f9afea16180514dde65b639f4&var-config1=build-coq.8.17.0-timing&var-branch2=time%2Fkeep_sidecond_in_goal&var-commit2=6946308078465f20d49245f3eb486eb60217afcd&var-config2=build-coq.8.17.0-timing&var-metric=instructions&var-group=%28.%2A%29https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/160Make existentials more lazy2023-07-31T14:24:38ZMichael SammlerMake existentials more lazyTiming gets worse, but it is not bad: https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=refinedc&var-branch1=master&var-commit1=4f0ad0efffb973e77de370367d0785027e5ed6cc&var-config1=build-coq.8.17.0-timing&var-bran...Timing gets worse, but it is not bad: https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=refinedc&var-branch1=master&var-commit1=4f0ad0efffb973e77de370367d0785027e5ed6cc&var-config1=build-coq.8.17.0-timing&var-branch2=time%2Flazy_ex&var-commit2=3ba9876efb0884f13fd3a01abb54cffbefa78cbb&var-config2=build-coq.8.17.0-timing&var-metric=instructions&var-group=%28%29.%2A
For Islaris, this MR even improves performance: https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?from=1690301582547&to=1690813398415&var-metric=instructions&var-project=isla-coq&var-branch=All&var-config=All&var-group=%28%29.%2A