Add deletionIsSafe2 assert to deleteObjects

[michaelmcinerney]

Maybe the commit message could do with some elaboration. I can add something if so.

This currently includes a commit from the "yet more rules for Lib" PR, so should be merged after that PR is merged.

[michaelmcinerney]

Using schact_is_rct in some of the top level theorems is actually a bit of a nuisance. I will attempt to redo some of this with as few changes to lemma statements as possible, to hopefully make other sessions like InfoFlowC pass without any further changes. I'll force push a change soon, and it would be best to hold off reviewing until then, though the change should be small

[michaelmcinerney]

Tests are passing, and this is ready for review now.

I went back and forth on where the schact_is_rct definition should be used. I think all the uses of it that were upsetting InfoFlowC were in Syscall_R, so I could probably use schact_is_rct in Refine.thy without upsetting anything else. But getting it all working was super annoying, so I'd rather leave it as is

[Xaphiosis]

It's probably too much to hope for, but do these assertions have any more specificity now that there's two of them? I'm worried about the essay_version4_final(3)_final.doc effect. Reading it as a reviewer I have no clue what they'd be, but I guess we can live with it.

[michaelmcinerney]

The comment just before deletionIsSafe does talk a little bit about their intent. I could be more precise, but it's one of those situations where I would be referencing something that happens within the Isabelle theory files, and so if the definitions change there, the comment becomes outdated.

As for why there are two asserts, again the comment before these definitions is trying to say that there are two because they're proved by different means. Maybe I could slightly strengthen the comment to say "We separate these properties into two assertions only because they are shown to be true by different means."

[Xaphiosis]

The thing is, when a reviewer goes over your diff and doesn't have a good idea of what's happening or why, you're going to get comments that aren't very smart from the author's perspective. This is one of those times. I just don't get what's going on with the two asserts, and how they're shown by different means :/
It's a bit of an art to figure out whether it makes sense to put in enough info to explain that, or whether it's hopeless. My instinct says that if you added a separate assertion rather than meld it into the previous one, then it deserves a better name than 2. Especially now that you explained the reasoning behind the + above, your goal is to be able to add more assertions... then it wouldn't be super nice if we had the infrastructure, but they ended up named 3, 4 etc. That's what I mean by the essay_version4_final(3)_final.doc effect, but it's hard to communicate over text.

[michaelmcinerney]

The first assert is shown to be true in the lemma deletionIsSafe (terrible name...) which is in the detype_locale'. The second assert is shown to be true in the lemma deletionIsSafe2_holds in delete_locale. These locales aren't comparable, so there's no nice way of proving them in one go, hence their separation.

Yes I could come up with more specific names for these asserts, but the first assert seems like a bit of a grab bag of properties that we want to hold for deletion. I would have simply added another conjunct instead of writing a new assert had it been straightforward to prove it all in one go. If you think I should change the name, I can. Maybe live_detype or something more longwinded and more ugly

[Xaphiosis]

Cool, that helps me understand what's going on, thanks.
Maybe when democracy rolls over this review, they'll have more ideas. How about renaming deletionIsSafe2 to deletionIsSafeLiveDetype or something like that (_live_detype can also work)? The first deletionIsSafe is historically a grab-bag already, renaming that is probably a waste of effort.

[michaelmcinerney]

I'd be happy with your suggestion. Maybe we'd like to make the 2 version a grab bag for other properties that are proved in the same way, in which case we're back to having no good specific name, but I suppose we can cross that bridge when we come to it

[Xaphiosis]

Cool. If it comes to that, it'll either be in the first grab bag, the same locale (thus might not need a rename), or a different one which would require a new assert.

[lsf37]

I do share the concern that 2 is not a helpful name. Would it be future-proof-ish to postfix with the locale the second one is proved in? (I haven't reviewed that bit yet in the proofs).

[Xaphiosis]

I'm fine with the changes, but would appreciate more information as to why stuff is happening. With nothing in the commit message, and not much in the PR description, I'm left with this vibe of reading the diff to figure out why I'm reading the diff. Probably you discussed it with someone else and they have it fresh in their memory, but in a year that won't be the case.

In particular, for expanding the commit message, as a reviewer who is a bit of an outsider on this:

• you're changing an invariant definition, to wrap up a specific term, would
  be useful to know that before having to look through a large diff
• why is this needed, when it was not needed before? it doesn't seem to have anything directly to do with your assertion that's in the commit message (does not appear in the assertion definition)
• you're adding a second assertion instead of expanding the first, why?

This would also be useful to know before starting to review the PR (usually PR description can be derived from commit message(s)).

I didn't put feedback on every instance of something, so if you do address it, don't forget it applies to the other arches too.

Oh, and it's impressive how fast you're pushing this stuff through, just don't forget to leave some breadcrumbs for those catching up. Thanks.

[michaelmcinerney]

I'm fine with the changes, but would appreciate more information as to why stuff is happening. With nothing in the commit message, and not much in the PR description, I'm left with this vibe of reading the diff to figure out why I'm reading the diff. Probably you discussed it with someone else and they have it fresh in their memory, but in a year that won't be the case.

Yes this was discussed on Mattermost a couple of weeks back. It came out of the work for linked lists. For that work, I did want to follow along with the reasoning I used on the rt branch for dealing with the tcbSchedNext and tcbSchedPrev pointers that are now in the TCB object, and the separate assert for master was the easiest way of going about this. Gerwin mentioned that it would be best if these changes could be done separately for master, which is why I've put this PR up, but unfortunately, there's nothing currently in master that necessitates this change. Should I mention in the commit message "an assert regarding object deletion for live objects is added, in preparation for future changes to the TCB object" or something like that?

In particular, for expanding the commit message, as a reviewer who is a bit of an outsider on this:

• you're changing an invariant definition, to wrap up a specific term, would
  be useful to know that before having to look through a large diff

What is the invariant definition that I'm changing? This should just be adding an assert and reshuffling Detype_R to accommodate it

• why is this needed, when it was not needed before? it doesn't seem to have anything directly to do with your assertion that's in the commit message (does not appear in the assertion definition)

Let me know if my "in preparation for future changes" idea above is a good one

[Xaphiosis]

I'm fine with the changes, but would appreciate more information as to why stuff is happening. With nothing in the commit message, and not much in the PR description, I'm left with this vibe of reading the diff to figure out why I'm reading the diff. Probably you discussed it with someone else and they have it fresh in their memory, but in a year that won't be the case.

Yes this was discussed on Mattermost a couple of weeks back. It came out of the work for linked lists. For that work, I did want to follow along with the reasoning I used on the rt branch for dealing with the tcbSchedNext and tcbSchedPrev pointers that are now in the TCB object, and the separate assert for master was the easiest way of going about this. Gerwin mentioned that it would be best if these changes could be done separately for master, which is why I've put this PR up, but unfortunately, there's nothing currently in master that necessitates this change. Should I mention in the commit message "an assert regarding object deletion for live objects is added, in preparation for future changes to the TCB object" or something like that?

Yeah, but, your use of English is excellent and better than mine, can you try make it a bit... less minimal? As in convey some of the above, now that you already have the text. It's preparatory work to switch the design spec ready queues over to next/prev pointers in TCBs, but I'm missing some knowledge on how these changes relate to that. Anything interesting on why we need the live for the delete?

I like something like "Add assert regarding object deletion for live objects" but would appreciate an expansion of the second half. I realise it might be hard to think in terms of "what does someone who didn't do this work want to know", but I'm trying to convey that it was difficult to make sense of this PR until reading through the entire diff and getting some answers from you.

In particular, for expanding the commit message, as a reviewer who is a bit of an outsider on this:

• you're changing an invariant definition, to wrap up a specific term, would
  be useful to know that before having to look through a large diff

What is the invariant definition that I'm changing? This should just be adding an assert and reshuffling Detype_R to accommodate it

Uhh, I saw theorem about callKernel preconditions, did I get confused? That's why I'm saying some info is useful before the review starts. Now I'm starting to remember some work for domain ticks I did ages ago... you're right these conditions aren't invariant. See what I wrote in another comment about potentially silly sounding comments by confused reviewers.

• why is this needed, when it was not needed before? it doesn't seem to have anything directly to do with your assertion that's in the commit message (does not appear in the assertion definition)

Let me know if my "in preparation for future changes" idea above is a good one

Yes, good idea, I encourage you to step a bit harder on the gas pedal :)

[michaelmcinerney]

Yeah, but, your use of English is excellent and better than mine, can you try make it a bit... less minimal? As in convey some of the above, now that you already have the text. It's preparatory work to switch the design spec ready queues over to next/prev pointers in TCBs, but I'm missing some knowledge on how these changes relate to that. Anything interesting on why we need the live for the delete?

It's already the case that no live object exists in the region to be detyped, but I think I did want this to be known explicitly within the proof of deleteObject_corres. Not that the following explanation will be of any use in the commit messages, seeing that they won't be able to see the definitions of live', but an object will (soon) be live' if the tcbSchedPrev or tcbSchedNext pointer is not None. I think I wanted the assert in order to make some arguments about what object deletion does to the heap projections tcbSchedNexts_of/tcbSchedPrevs_of so that we can show that deleteObjects establishes ready_queues_relation.

I like something like "Add assert regarding object deletion for live objects" but would appreciate an expansion of the second half. I realise it might be hard to think in terms of "what does someone who didn't do this work want to know", but I'm trying to convey that it was difficult to make sense of this PR until reading through the entire diff and getting some answers from you.

Yes I thought that the Mattermost discussion would have been enough background for this PR but I guess it wasn't. Sorry about that.

Uhh, I saw theorem about callKernel preconditions, did I get confused? That's why I'm saying some info is useful before the review starts. Now I'm starting to remember some work for domain ticks I did ages ago... you're right these conditions aren't invariant. See what I wrote in another comment about potentially silly sounding comments by confused reviewers.

This does rearrange some scheduler_action statements into schact_is_rct but that's about all that's changed for the top level theorems.

[Xaphiosis]

...
It's already the case that no live object exists in the region to be detyped, but I think I did want this to be known explicitly within the proof of deleteObject_corres. Not that the following explanation will be of any use in the commit messages, seeing that they won't be able to see the definitions of live', but an object will (soon) be live' if the tcbSchedPrev or tcbSchedNext pointer is not None. I think I wanted the assert in order to make some arguments about what object deletion does to the heap projections tcbSchedNexts_of/tcbSchedPrevs_of so that we can show that deleteObjects establishes ready_queues_relation.

That's a pretty good explanation. I would not mind something like this ("a TCB will (soon) be live' if the [next/previous queue pointers] ...", combined with our discussion above) if it makes it into a commit message.

I like something like "Add assert regarding object deletion for live objects" but would appreciate an expansion of the second half. I realise it might be hard to think in terms of "what does someone who didn't do this work want to know", but I'm trying to convey that it was difficult to make sense of this PR until reading through the entire diff and getting some answers from you.

Yes I thought that the Mattermost discussion would have been enough background for this PR but I guess it wasn't. Sorry about that.

Could be my bad, lots of mattermost messages + deadlines.

Uhh, I saw theorem about callKernel preconditions, did I get confused? That's why I'm saying some info is useful before the review starts. Now I'm starting to remember some work for domain ticks I did ages ago... you're right these conditions aren't invariant. See what I wrote in another comment about potentially silly sounding comments by confused reviewers.

This does rearrange some scheduler_action statements into schact_is_rct but that's about all that's changed for the top level theorems.

Cool. Maybe drop that in the commit message with the argument that it's to match rt/mcs.

[michaelmcinerney]

Now with a new and improved commit message. I didn't want to go into too much detail about which fields I'll be adding to the TCB object, but I hope that what I have here is informative enough

[lsf37]

Modulo the name discussion and the mask_range usage for the definition of the assertion, I'm happy with this as is.