search

PrincetonUniversity / VST

Verified Software Toolchain
https://vst.cs.princeton.edu
Other
424 stars 91 forks source link

VST on Iris #755

Open mansky1 opened 3 months ago

mansky1 commented 3 months ago

Replaced MSL with Iris, rebuilt VeriC and Floyd on top of it.

mansky1 commented 3 months ago

@andrew-appel I'm now working on getting this to pass the CI -- it currently works only for 8.17 and 64-bit mode. Which Coq versions and bitsizes does it need to pass? (I'd prefer not to have to support 8.16, if that makes sense.)

andrew-appel commented 3 months ago

Not necessary to support 8.16. If you can support 8.18 and newer, that will be good enough for any release AFTER April of 2024, which will (presumably) be for a Coq Platform for Coq 8.20.

andrew-appel commented 3 months ago

But please do support 32-bit mode.

mansky1 commented 3 months ago

Okay! It looks like the main obstacle to supporting 32-bit mode will simply be maintaining all of the examples -- list_dt is messy and hasn't been touched in years, and there are a bunch of other examples that aren't in 64-bit and aren't quite trivial to port. I'll do as many as I can in the next few weeks, but I'd love to know if there are any programs in progs that don't really need to be in the CI.

andrew-appel commented 3 months ago

Aside from the 32-bit question, how fast is the performance of VST-Floyd in this branch, compared to the master branch?

mansky1 commented 3 months ago

The slowdown on the CI tests is between 0% and 60%. At the level of individual tactics, forward is sometimes equal or faster, sometimes 3-4x slower. Most of the remaining slowdown is from autorewrite (esp. in normalize). I can't tell how much of that is inevitable and how much could be improved, because I have no idea how to get diagnostics on autorewrite (basically I want this but it seems not to have happened).

mansky1 commented 3 months ago

By the way, it looks like this anomaly is crashing some of my tests on Coq 8.18.0 specifically. It appears to be fixed in 8.18.1, but I don't know how to change the CI to test on that instead (just changing 8.18 to 8.18.1 in coq-action.yml didn't work).

mansky1 commented 2 months ago

Status update: Reduced the slowdown considerably. Some 8.18 tests still fail due to a bug (and 8.18.1 doesn't actually exist yet). I haven't made much progress on test5 (VSUs), but everything else is working.

andrew-appel commented 1 month ago

My most recent commit c4a2d30 brings @lennartberinger's recent proofs about VSU dry safety into the vst_on_iris branch, all commented out. I wonder how difficult it will be to uncomment and port these to the vst_on_iris model.