Skip to content

VST on Iris#755

Draft
mansky1 wants to merge 593 commits into
masterfrom
vst_on_iris
Draft

VST on Iris#755
mansky1 wants to merge 593 commits into
masterfrom
vst_on_iris

Conversation

@mansky1

@mansky1 mansky1 commented Mar 4, 2024

Copy link
Copy Markdown
Collaborator

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

@mansky1

mansky1 commented Mar 19, 2024

Copy link
Copy Markdown
Collaborator Author

@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

andrew-appel commented Mar 22, 2024

Copy link
Copy Markdown
Collaborator

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

andrew-appel commented Mar 22, 2024

Copy link
Copy Markdown
Collaborator

But please do support 32-bit mode.

@mansky1

mansky1 commented Mar 22, 2024

Copy link
Copy Markdown
Collaborator Author

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

andrew-appel commented Mar 22, 2024

Copy link
Copy Markdown
Collaborator

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

@mansky1

mansky1 commented Mar 22, 2024

Copy link
Copy Markdown
Collaborator Author

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

mansky1 commented Mar 22, 2024

Copy link
Copy Markdown
Collaborator Author

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

mansky1 commented Apr 4, 2024

Copy link
Copy Markdown
Collaborator Author

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.

mansky1 and others added 30 commits February 27, 2025 09:43
@mansky1
Update ivst.md
412a1bd
@mansky1
Update ivst.md
2ea464e
@ducthann
WIP on semax_to_dry_machine.v
bd81ab5
@mansky1
fixed change_compspecs
b3b7955
@mansky1
Merge branch 'vst_on_iris' of https://github.com/PrincetonUniversity/VST
46e79d4 
 into vst_on_iris
@mansky1
consistent type annotations for atomic notations
475d0d2
@mansky1
remove ora submodule; should install coq-vst-ora via opam instead
835680c
@mansky1
Update README.md
a4be1f5
@mansky1
propagate lock_t change to incrN
59d276b
@mansky1
Merge branch 'vst_on_iris' of https://github.com/PrincetonUniversity/VST
4e4f15c 
 into vst_on_iris
@Mathtician @claude
fix builddep: align dependency versions
a6ffe0a 
Bump coq to >= 8.19 & < 8.21 to agree with the Makefile, and add the
required coq-iris and coq-vst-ora (= 1.0; 1.1 does not work) dependencies.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@mansky1
Merge pull request #856 from Mathtician/vst_on_iris
57af496 
fix builddep: align dependency versions
@mansky1
WIP: merging master
89ecaef
@mansky1
merge builddep
f6a9bee
@mansky1
updated through lifting
9392a6b
@mansky1
finished merging veric and floyd
bdf7ff6
@mansky1
clean up warnings; basic examples work
9dba59e
@mansky1
update extended examples
0850e13
@Mathtician
add atomic machine (first draft)
e7f8d83
@Mathtician
Revert "add atomic machine (first draft)"
479769d 
This reverts commit e7f8d83.
@Mathtician
Reapply "add atomic machine (first draft)"
4364544 
This reverts commit 479769d.
@mansky1
Merge pull request #859 from Mathtician/atomic_machine
2c62d64 
Atomic machine
@mansky1
list-based claim and commit
18ad822
@dkxb
add option to use cascompcert as VST's compcert option
678ec37
@dkxb
include alloc and free in memory event definition; (somewhat) general…
de6d021 
…ize the type of values and locations
@dkxb
add translation from event_semantics events to atomic machine events
abd7f87
@dkxb
change unrsv to fin; rw_map for Free should be updated at fin time
341a66a
@dkxb
use the bundled Clight in makefile
8cadf5e
@dkxb
update build instructions, allow for dev version of ora
d502ee1
@mansky1
Merge pull request #863 from dkxb/at_sem
c3a9fbe 
Updates on atomic_semantics
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@mansky1 @andrew-appel @ducthann @dkxb @Mathtician