Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

ccorres rules for the reply functions #881

Merged
merged 6 commits into from
Apr 4, 2025
Merged

ccorres rules for the reply functions #881

merged 6 commits into from
Apr 4, 2025

Conversation

michaelmcinerney
Copy link
Contributor

Test with seL4/seL4#1440

@lsf37 @michaelmcinerney
proof: adjust for config_set wrapper in C
ad6e5cf 
config_set conditions are now wrapped in an inline function in C so that
corresponding "if" statements are not automatically rewritten by
ccorres. Adjust proofs accordingly.

For most instances, we execute the inline function and call
ccorres_rewrite to get the same proof state as before. We can then later
add new specification and proof branches for these config options.

Signed-off-by: Gerwin Klein <[email protected]>
@michaelmcinerney michaelmcinerney added the MCS related to `rt` branch and mixed-criticality systems label Apr 1, 2025
@michaelmcinerney michaelmcinerney self-assigned this Apr 1, 2025
@lsf37
Copy link
Member

lsf37 commented Apr 1, 2025

To get rid of the link check failure, cherry-picking commit 9a28f50 should work.

lsf37
lsf37 reviewed Apr 1, 2025
View reviewed changes
Copy link
Member

@lsf37 lsf37 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I realise this was still in draft, apologies for jumping in early with the comments. If we can resolve those instantiation chains, I think this is pretty much ready to go.

@michaelmcinerney michaelmcinerney marked this pull request as ready for review April 1, 2025 23:29
@Xaphiosis
Copy link
Member

Minor question on commit (message are generally good and helpful, thank you):
In rt haskell+riscv refine+crefine: ccorres rules for reply, the tag is kind of confusing. @lsf37 ?

@lsf37
Copy link
Member

lsf37 commented Apr 2, 2025

Minor question on commit (message are generally good and helpful, thank you): In rt haskell+riscv refine+crefine: ccorres rules for reply, the tag is kind of confusing. @lsf37 ?

It is trying to say generic Haskell and RISCV refine+crefine. Maybe in this case we should just shorten in to rt haskell+refine+crefine

Xaphiosis
Xaphiosis reviewed Apr 2, 2025
View reviewed changes
proof/crefine/RISCV64/IpcCancel_C.thy
apply (rule conseqPre, rule conseqPost)
apply assumption
apply clarsimp
apply (rule rev_bexI, rule updateSchedContext_eq)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

clarsimp should discharge the assumption, then we have clarsimp, three simps, and a clarsimp... I think you can safely put a ; clarsimp simp: obj_at_simps at the end here and save some lines

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(or clarsimp with a +)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These were just moved. I meant to write a nicer PR description before I marked this as ready for review. But these updateSchedContext_ccorres_* lemmas were just moved, along with schedContext_donate_ccorres and tcbReleaseRemove_ccorres

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's still a pretty easy compression if you're interested while we're here.

Xaphiosis
Xaphiosis approved these changes Apr 2, 2025
View reviewed changes
Copy link
Member

@Xaphiosis Xaphiosis left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think Gerwin already found the interesting issues. When he's happy with it, don't wait up for me. I definitely agree that postcondition instantiation pattern is not great for maintenance, and some way of automating our way out of it should be explored.

@Xaphiosis
Copy link
Member

Minor question on commit (message are generally good and helpful, thank you): In rt haskell+riscv refine+crefine: ccorres rules for reply, the tag is kind of confusing. @lsf37 ?

It is trying to say generic Haskell and RISCV refine+crefine. Maybe in this case we should just shorten in to rt haskell+refine+crefine

Yeah I think we'd normally have two commits, one for spec changes and one for proof update. In this case, I'd probably go with your suggestion given the nature of the rt tag.

@michaelmcinerney
Copy link
Contributor Author

I've pushed an update with the fix for the broken links, a commit that reduces the use of valid_objs' in CRefine, and another commit that removes the nasty hoare_post_imp chains that I had in the ccorres rules for the reply functions. The changes to get rid of valid_objs' were a bit larger than I was hoping for, but it should really make life easier in CRefine (apart from potentially having to add the assert to more new functions)

@michaelmcinerney
Copy link
Contributor Author

I think I missed a few updates for the new asserts, so I'll run the proofs again locally and push an updated version soon.

@michaelmcinerney michaelmcinerney force-pushed the michaelm-reply_functions branch 2 times, most recently from 5f6f140 to f6e43d9 Compare April 3, 2025 10:01
Xaphiosis
Xaphiosis approved these changes Apr 3, 2025
View reviewed changes
Copy link
Member

@Xaphiosis Xaphiosis left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks like you were on the right track with the valid_objs' crossing, and the proofs look neater now.

lsf37 and others added 3 commits April 4, 2025 10:48
@lsf37 @michaelmcinerney
link check: new file for ignoring URLs and files
901ab85 
Signed-off-by: Gerwin Klein <[email protected]>
@michaelmcinerney
rt crefine: use option_to_ctcb_ptr and from_bool in creply_relation
a92eb5c 
The replyTCB field of a reply points to a TCB, and so should use
option_to_ctcb_ptr, rather than option_to_ptr.

Additionally, from_bool is preferred to to_bool.

Signed-off-by: Michael McInerney <[email protected]>
@michaelmcinerney
rt crefine: weaken guard in reply_unlink_ccorres
58deef5 
Signed-off-by: Michael McInerney <[email protected]>
@lsf37
Copy link
Member

lsf37 commented Apr 4, 2025 

 Installing seL4 python deps
    error: subprocess-exited-with-error

I'm coming to really dislike Python. Ok to ignore this here, it's some setup problem of the style checker.

lsf37
lsf37 approved these changes Apr 4, 2025
View reviewed changes
Copy link
Member

@lsf37 lsf37 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Agreed, the valid_objs' idea was good. We have a bit of the post condition instantiation moving into Refine, but now concentrated to just once and also in a nicer form. I like it.

@michaelmcinerney
rt haskell+refine+crefine: ccorres rules for reply functions
ab750ae 
This proves the ccorres rules for all functions which directly
modify the reply objects, namely reply_pop, reply_push, reply_remove,
and reply_remove_tcb.

This refactors the Haskell definitions slightly:

 - the when statement in replyPop is removed, since replyPop is
   called only from replyRemove, which contains an explicit check
   for the condition in the when statement.

 - the call to cleanReply in replyPop is removed and replaced with
   an update of the replyPrev field to Nothing. This preserves
   semantics, since the replyNext field is set to Nothing earlier
   in the function.

 - updateSchedContext is preferred to setSchedContext.

Signed-off-by: Michael McInerney <[email protected]>
@michaelmcinerney
rt haskell+refine+crefine: reduce use of valid_objs' in CRefine
eeb3165 
Signed-off-by: Michael McInerney <[email protected]>
@michaelmcinerney michaelmcinerney force-pushed the michaelm-reply_functions branch from f6e43d9 to eeb3165 Compare April 4, 2025 01:09
@lsf37
Copy link
Member

lsf37 commented Apr 4, 2025 

 Installing seL4 python deps
    error: subprocess-exited-with-error

I'm coming to really dislike Python. Ok to ignore this here, it's some setup problem of the style checker.

And it now works on the same OS and python version without anything having changed. Maybe it was a networking problem or something like that.

@lsf37 lsf37 merged commit ef0f2e8 into rt Apr 4, 2025
11 checks passed
@lsf37 lsf37 deleted the michaelm-reply_functions branch April 4, 2025 04:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Xaphiosis Xaphiosis Xaphiosis approved these changes

@lsf37 lsf37 lsf37 approved these changes

@corlewis corlewis Awaiting requested review from corlewis

Assignees

@michaelmcinerney michaelmcinerney

Labels
MCS related to `rt` branch and mixed-criticality systems
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@michaelmcinerney @lsf37 @Xaphiosis