More uniformly handle endpoint and notification queues - Haskell and Refine

[michaelmcinerney]

No description provided.

[michaelmcinerney]

Force pushed (a few times...) to remove some .marks files and remove trailing whitespaces.

[lsf37]

I still have the urge to rename rule, because at the use side it is not going to be clear what kind of rule and what we're solving (wp and simp are clear enough). The problem is that it's multi-purpose. Maybe we should call it at least intro, since it's always used as an intro rule even though it's not a general-purpose intro rule.

Not sure. Any other opinions?

[michaelmcinerney]

I don't have any strong opinions on this one, except that I would hope that if someone were wanting to use the method and wanted to know how it did work, they would read the comment. Maybe a big hope. If it helps, I could make the comment a bit more explicit by saying "so that the side conditions for the abstract monad such as..." Or "abstract monadic function". I'm never sure which is correct.

[lsf37]

It's not so much about wanting to use the method, but understand what is written when you see the method used (and then maybe working from example).

[michaelmcinerney]

OK, then I'm really not so sure. This rule: bit here is for what we might call "side-conditions", so maybe we could do something a bit out of the ordinary like side: ?

[lsf37]

As a user that still doesn't tell me in which kind of context these rules are going to be applied. Is it correct that they are all about side conditions for rcorres_lift rules? Maybe something in that direction, but we'd need to be careful to not make it sound like we're supplying the actual lifting rule there (unless we do).

[michaelmcinerney]

Yes these will all be side conditions for rcorres_lift rules, and so will be either a det_wp, no_fail, or empty_fail rule about the abstract function in the rcorres statement. I think side: or something else unusual will be a good prompt for people to look into the details, but still not sure.

[lsf37]

Suggested change

	apply (rule relatedE, fastforce, ko, ako, simp add: tcb_relation_cut_def)
	apply (rule relatedE, fastforce, ko, ako, simp add: tcb_relation_cut_def)

[lsf37]

We should not completely get rid of the inline comments. It's clear to us what the constructors mean, but that SendEP state is for waiting on send operations to complete should be a comment (same for receive). Doesn't have to be LaTeX, could probably be a -- comment after each constructor.

[lsf37]

(same as the EP comments above)

[lsf37]

These should get comments on what they are and under which circumstances we expect them to have values (queue empty when idle, non-empty when not; msgIdentifier Some iff Active)

[michaelmcinerney]

Sure, I can do that. But doesn't the same thinking apply to all the kernel objects? And if we were to change what valid_ntfn' says in the future (I changed it about half a dozen times while I was doing this work) then the comment gets out of date and so on.

[lsf37]

The comment doesn't have to mirror valid_ntfn' precisely (although it's probably roughly those concepts). It is true that comments need to be updated with change, but the Haskell code is the main documentation source for the code, so if we have code comments, this is where they should be. Most other kernel object types do not actually have many of these internal consistency conditions, because we are usually trying to express these by type. Here we have chosen to more closely mirror the C where the object can have internally inconsistent states, so we want to a) call that out and b) document what we expect for internal consistency.

[lsf37]

The canonical name here would be isBlockedOnNotification. It's a lot to type, but I think it would be cleared in code where we don't immediately see if the test is on a kernel object or a thread state.

[michaelmcinerney]

This is named in analogy with isSend and isReceive just above. Should I just fix this one, or fix all of them, while I'm here?

[lsf37]

Those two at least can't be confused with kernel objects, but it would make sense to stick to the regular names. Not sure how often they are used. Change it only if it's not too much noise.

[michaelmcinerney]

I did make these changes, but now I'm getting a clash of names with the name produced automatically in spec/design/Structures_H.thy. I guess this is why they were called isSend and isRecv to begin with. Maybe we could stick with isSend and isRecv and then go with isBlockedOnNtfn rather than the isBlockedOnNotification. Or is there a way to suppress some of these definitions being produced automatically?

[lsf37]

Right, that is annoying. Those automatic declarations were supposed to help not produce noise. Let's stick with the isSend and isRecv, and I like isBlockedOnNtfn. The "real" fix would be to make the Haskell generator suppress the other definitions, but I don't think we should try that here.

[lsf37]

These were there before, but if we're changing things anyway we might as well get rid of the C-isms in Haskell.

Suggested change

	> if (call || isJust fault)
	> then if ((canGrant || canGrantReply) && replyOpt /= Nothing)
	> if call || isJust fault
	> then if (canGrant || canGrantReply) && replyOpt /= Nothing

[lsf37]

Suggested change

	> test <- if (tcbQueueEmpty q)
	> test <- if tcbQueueEmpty q

[lsf37]

Suggested change

	> if (r endVal val)
	> if r endVal val

[lsf37]

Suggested change

	objects of some type are in a particular relation, in the case where for every abstract kernel
	objects of some type are in a particular relation. Applies where for every abstract kernel

[lsf37]

Do you depend on the formulation with { .. | ..} in the proof a lot? Because it is a bit strange with UNIV on the right-hand side. Could be written as (%y::pt_index. p + (ucast y << pteBits)) ' UNIV for instance. Maybe there is an even shorter way.

[lsf37]

Then again, maybe it is nicer to keep it analogous to the other definitions.

[michaelmcinerney]

I don't think I depend on this formulation in the proof. I'd be happy to write whatever here. The main thing is to get pspace_relation written in terms of the smallest heaps possible, so the actual definitions don't bother me much at all.

[lsf37]

This is one of these "too hard to decide, because it's not really that important" things. Let's leave it as is unless others have strong opinions about it.

[lsf37]

Now that the work is done, what do you think, should it take aobjs_of instead? Although we should probably wait for the full arch split on this, because AARCH64 or X64 might have other things that might flow in here, e.g. from ghost state.

[michaelmcinerney]

Since we have those pesky userData_at and userDataDevice_at heaps to consider as well, it can't be just in terms of aobjs_of, which might make that idea less appealing. I like the way it is at the moment, and I think the arch-split machinery should still work well with this approach, though I'm of course not the best person to make that judgement call.

[lsf37]

You're right about userData_at and userDataDevice_at, and for arch split I don't think it matters which one we choose. In that case, we can probably remove the comment.

[lsf37]

This is a generic (non-arch) statement. Does the proof need anything arch-specific, or could this live in a generic file? (same for the other arch-generic object types)

[lsf37]

I see there is an arch_kernel_obj.split_asm in the proof. Do we actually need it? If yes, an arch split comment would be good so that we can look into it in the future.

[michaelmcinerney]

I know that this does include at least obj_relation_cuts_def2, which is an arch lemma. During the Zoom call when we were discussing these things, Raf said that this was a big pain to deal with.

[lsf37]

It is. Ok, let's put a comment there that this uses the arch kernel object split and obj_relation_cuts_def2, so can't currently be generic. (With a FIXME: arch-split). Then we can find them again if/when we figure something out.

[lsf37]

This is not a good [elim] rule, the rhs is unlikely to match. We could make it an [elim!] or [dest!] rule if we made ksPSpace s' p = Some KOKernelData the major (first) premise.

[michaelmcinerney]

OK sure. I actually don't know what the reasoning is for what should or should not be [elim] or [dest!] or whatever. What is the thinking behind all this?

[lsf37]

elim rules are generally of the form [| E; Q ==> P |] ==> P where P is a free P, E is a complex term that should be eliminated in the assumptions (hence the name) and replaced by Q. The tools that understand elim match simultaneously on the major premise E and the conclusion P.

We often use the degenerated form E ==> P where P is not free. That works for cases where both E and P occur simultaneously and the rule solves the goal. For that to work P must be something that actually occurs in conclusions of goals.

[dest] will take a rule [| D; ... |] ==> P and match on D only, in the assumptions of the goal, destroying D in those assumptions, and replacing it by P (and adding subgoals for any ...).

[michaelmcinerney]

Great, thanks.

[lsf37]

So in the case above, if the rule is written as

[| ksPSpace s' p = Some KOKernelData; heap_pspace_relation s s' |] ==> False

then at least it is more likely to match. Whether it should be [elim] or [elim!] is a separate question. If we are confident that we will always have heap_pspace_relation in the goal or something we can derive heap_pspace_relation from when KOKernelData appears, then we can mark the rule as safe ([elim!]). Otherwise we shouldn't (i.e. we should leave it on just [elim]), because it would produce potentially unprovable heap_pspace_relation goals.

[michaelmcinerney]

Right, I at first wasn't thinking so much about simplification having occurred on the rhs.

You don't need to answer this right now, but why do we have things like valid_sched s ==> valid_release_q s as [elim!]? We don't always have valid_sched s in the premisses when we have valid_release_q s as the conclusion.

[lsf37]

elim matches major premise and conclusion simultaneously, so if there is nothing else in the rule, which means that it will solve the goal, then it is safe. For intro where it only matches the conclusion, it would not be safe.

[lsf37]

Are these slow fastforce? If not, these should all be apply/done.

[michaelmcinerney]

Yes all the bys in this file are a bit slow, maybe 2-3 seconds or thereabouts.

[lsf37]

These last rules all have the form

  "⟦⋀s'. no_fail (λs. Q s s') f; empty_fail f;
    ⋀P s'. ⦃λs. P (p s) ∧ Q s s'⦄ f ⦃λ_ s. P (p s)⦄;
    ⋀P s. ⦃λs'. P (p' s') ∧ Q s s'⦄ f' ⦃λ_ s'. P (p' s')⦄⟧
   ⟹ rcorres
         (λs s'. p s = p' s' ∧ Q s s')
         f  f'
         (λ_ _ s s'. p s = p' s')"

Would that be provable on its own so that we can all just make them instances by setting p and p'?

[lsf37]

I suppose instead of = we could generalise to H (p s) (p' s')

[michaelmcinerney]

Good idea, I'll go with that, thanks.

[lsf37]

If this is actually necessary, then this is not a good sign. It means that name space priority has flipped in this PR because of changed theory imports, and that should definitely be avoided. In either case, it should never be kernel_object, but always Structures_A.

If it had actually flipped, I would expect more change to be necessary, so hopefully this can just be left out. If it can't, we need to find the import that has changed the naming.

[michaelmcinerney]

It's definitely necessary to write either kernel_object. or Structures_A. to get the aspec level one. I think this is similar to what we've had for Structures_A.kernel_object and thread_state before, so it doesn't seem unusual to me. But I'll go with Structures_A. everywhere it's necessary.

[lsf37]

But it wasn't necessary before, right? The line changes Notification to kernel_object.Notification which indicates that something as changed in how the names are processed, if a bare Notification was fine before. This is majorly bad. Have we changed the theory import structure anywhere?

[michaelmcinerney]

I haven't opened up the current version of rt to see exactly what Isabelle produces, and this branch is still processing things at the moment, but I think the change comes from the definition of the Notification type in the Haskell:

data Notification = NTFN {

is what we had before, and I changed the name of the record or whatever it is (the RHS here) to Notification. Should I change it back? It's confusing because NTFN was used for the notification object which is just the idle/active/waiting data structure and doesn't contain the linked TCB/sc. Now there's no separate data structure in the Haskell and it's just one big thing.

[lsf37]

Suggested change

	\<Longrightarrow>rcorres
	\<Longrightarrow> rcorres

[lsf37]

Does this work or does delta_sym_refs apply to the generated goal again?

Suggested change

	apply (erule delta_sym_refs)
	by (auto simp: ko_at_state_refs_ofD get_refs_def2 pred_tcb_at_def obj_at_def valid_ep_def
	split: list.splits if_splits)
	by (auto simp: ko_at_state_refs_ofD get_refs_def2 pred_tcb_at_def obj_at_def valid_ep_def
	elim!: delta_sym_refs
	split: list.splits if_splits)

[michaelmcinerney]

Yep, this works, thanks.

[lsf37]

Suggested change

	= Structures_A.thread_state.BlockedOnSend epptr data"
	= Structures_A.BlockedOnSend epptr data"

[lsf37]

Suggested change

	by (rcorres_conj_lift \<open>fastforce\<close>
	rule: det_wp_tcb_append_set_notification simp: tcbAppend_def)+
	by (rcorres_conj_lift \<open>fastforce\<close>
	rule: det_wp_tcb_append_set_notification
	simp: tcbAppend_def)+

[lsf37]

apply/done

[lsf37]

apply/done

[lsf37]

Should this be apply/done?

[michaelmcinerney]

These final rcorres_conj_lift steps churn through the last dozen or so conjuncts in state_relation and do take a while. The rule: bit that we've been discussing sometimes does speed them up quite a lot, but they're not super fast.

[lsf37]

This probably holds as well and should be more general

Suggested change

	"valid_obj' (KONotification (ntfnQueue_update (\<lambda>_. q) ntfn)) s
	"valid_obj' (KONotification (ntfnQueue_update f ntfn)) s

[lsf37]

Please add a comment what construct is closed by this end

[michaelmcinerney]

I was able to remove this block, and consolidated a couple small interpertation blocks for emptySlot into one. I adjusted things a little bit further down in the file, too.

I was also able to remove some lemmas for suspend from the delete_one or delete_one_conc locales, but I could put these changes in a separate commit if you'd like.

[lsf37]

Would be fine to leave inside this commit, it'd just be good to know what end closes if it comes after a longer block of things, because there is no indentation for context/locale etc that would tell us.

[michaelmcinerney]

Sure, I think I touch only one end statement in this theory file now, and it has a comment with it. Let me know if it's OK.

[lsf37]

Should these ASpec properties move up to AInvs? Clearly, they are not needed there at the moment, but they might come in handy in the future. Doesn't have to be now, but the question is if we should tag them with a FIXME: move or not.

[michaelmcinerney]

I suppose we could move them to AInvs, but since these properties are used only in Refine, we could get into the annoying situation where we want to modify the properties for a proof in Refine, but the definition is in AInvs, which is a lot of back and forth. Maybe if we think that the definitions are solid and the rules we have are good, it would be harmless to move.

I also have ep_queues_blocked, ntfn_queues_blocked, ready_qs_runnable, and release_q_runnable that are also ASpec properties and are similar in being used only in Refine. These are all pared down versions of other invariants (namely sym_refs and valid_ready/release_q(s)). My strong preference is for large invariants to be conjunctions of smaller invariants, and for large invariants to be proved by proving invariance of the smaller invariants wherever possible. If we did want to do something like that for sym_refs or valid_ready/release_q(s), then we'd definitely want to move these new ones to AInvs. (My aborted attempt at sym_heaps was exactly this. I still think it's a good idea, though it'll take a fair bit of work for it to become nice to work with.)

[lsf37]

Yeah, I'm not sure either. Especially the having to jump back and forth between sessions aspect could be very annoying when we ever want to tweak anything. That is a good argument for leaving it.

[lsf37]

tag with FIXME: move

[lsf37]

This is a dangerous name. We already have ctes_of, and I'm not sure they are equivalent, because AFAIR, ctes_of also talks about the CTEs inside TCBs and this does not look like it does. Are we using this new ctes_of' anywhere? I haven't seen it yet, but I might have missed it. The definition here corresponds to the concept of real_cte_at, and it could make sense to have it in isolation, but it would have to be pretty special circumstances.

[michaelmcinerney]

I think this is currently used only in caps_relation and the associated lifting rule, just to get the heap version of pspace_relation. So again I don't really care about the name or its definition or anything. I'm happy to change it to whatever you'd like. It does seem a bit odd that just going by the name of the kernel object could cause confusion or be dangerous.

[lsf37]

That's because this kernel object is special -- it does precisely not induce its own heap in the same way the others do, at least not in the way the kernel actually uses these objects, because CTEs do not only occur directly in kheap, but also as part of TCBs. That does not happen for any other kernel object.

It works for the state relation, because you can still assert cap_relation separately for each tcb slot (which is what it does), but the rest of the proofs needs a unified TCB/CNode space of CTEs. So adding another CTE heap that only has the CNode space with a name that is practically the same as the existing unified one is asking for trouble.

Concretely I would call this one cnode_ctes_of' (prime so that we can do the same on ASpec at some point if we later want to).

[lsf37]

Suggested change

	apply (rule rcorres_from_valid_det; (solves wpsimp)?)
	unfolding tcbQueuePrepend_def list_queue_relation_def
	unfolding tcbQueuePrepend_def list_queue_relation_def
	apply (rule rcorres_from_valid_det; (solves wpsimp)?)

[lsf37]

unfolding is not meant to be used in the middle of an apply script.

Suggested change

	apply (rule rcorres_from_valid_det; (solves wpsimp)?)
	unfolding tcbQueueAppend_def list_queue_relation_def
	unfolding tcbQueueAppend_def list_queue_relation_def
	apply (rule rcorres_from_valid_det; (solves wpsimp)?)

(If you do want to unfold in the middle of an apply script, it should be apply (unfold ..), potentially with [1])

[lsf37]

Suggested change

	unfolding tcbQueueInsert_def list_queue_relation_def
	unfolding tcbQueueAppend_def list_queue_relation_def
	apply (rule rcorres_from_valid_det; (solves wpsimp)?)

[lsf37]

Suggested change

	apply (rule rcorres_from_valid_det; (solves wpsimp)?)
	unfolding tcbQueueRemove_def list_queue_relation_def
	unfolding tcbQueueRemove_def list_queue_relation_def
	apply (rule rcorres_from_valid_det; (solves wpsimp)?)

[lsf37]

apply/done?

[lsf37]

Would this work? I think that'd be slightly nicer (I'm assuming we need the pre for wps)

Suggested change

	apply (rule hoare_pre)
	apply (wps | wp assms | wpsimp wp: hoare_vcg_all_lift hoare_vcg_ball_lift hoare_vcg_imp_lift')+
	apply (wp_pre | wps | wp assms | wpsimp wp: hoare_vcg_all_lift hoare_vcg_ball_lift hoare_vcg_imp_lift')+

[lsf37]

(If that does work, there are a few more instances of this below)

[michaelmcinerney]

Doesn't work, unfortunately.

[lsf37]

apply/done

[lsf37]

Suggested change

	apply (wpsimp wp: set_simple_ko_wp)
	by (clarsimp simp: eps_of_kh_def opt_map_def)
	by (wpsimp wp: set_simple_ko_wp)
	(clarsimp simp: eps_of_kh_def opt_map_def)

(or sometimes moving the clarsimp content into wpsimp also works)

[lsf37]

apply/done

[lsf37]

Are the qualifiers necessary? I know they are used a lot in Refine, but that is mostly because Isabelle echoes them when there is a potential conflict. For a human reader, in lemmas like this it is pretty clear from context that it is the abstract side, and abstract names should have priority.

Suggested change

	tcb_state tcb = Structures_A.BlockedOnNotification ntfn_ptr\<rbrakk> \<Longrightarrow>
	\<exists>notification list. kheap s ntfn_ptr = Some (Structures_A.Notification notification)
	tcb_state tcb = BlockedOnNotification ntfn_ptr\<rbrakk> \<Longrightarrow>
	\<exists>notification list. kheap s ntfn_ptr = Some (Notification notification)

[michaelmcinerney]

These qualifiers are necessary. Not sure what's going on here if something is going wrong.

[lsf37]

We should investigate what is going on there and what naming scheme we want. I worry that we have accidentally flipped it (maybe not even in this PR), and that will just create a mess where eventually everything is qualified.

[lsf37]

I'd flag this for a FIXME: move next to threadRead_tcb_at'

[michaelmcinerney]

I can move this now.

[lsf37]

xs would the canonical name for a list. list is what comes out of the datatype name in Isabelle and doesn't really fit the naming conventions.

[lsf37]

In this case, I'd say ts (for threads) or even queue, although that also doesn't fit the naming convention. But at least later in the proof we'd know what kind of list it is.

[michaelmcinerney]

I think I called this list because it's the "list" of list_queue_relation. In the definition of ep_queues_relation, I use ls as the name of the green variable for the Isabelle list. Is ls bad there too and should I use ts instead?

[lsf37]

ls is uncommon, but acceptable. list is not a good name. The s is what signifies a list, l or list should not be used for that, because that gives you only precisely one list you can use at a time and then you've already run out of names and need ' or something else.

[lsf37]

I think the standard is actually with space. At least Raf always tells me to fix my operator spacing when I don't use it :-)

[michaelmcinerney]

I think Isabelle prints this without the space, so I'm never sure. I prefer with the space, personally, but I often default to what Isabelle does if I'm not sure. But I can change it.

[lsf37]

Isabelle print does print spaces for a \in A (it takes extra work to not make it print spaces for operators so it is very uncommon for there not to be a space in output)

[michaelmcinerney]

I've just double checked, and Isabelle will print a space for member, but won't print a space for Ball, the bounded universal quantifier.

[lsf37]

The indent looks off of the ob_at' condition. If it doesn't fit, I'd add a line break before obj_at

[michaelmcinerney]

I've rejiggered this a fair bit and it's a bit ugly but at least legible.

[lsf37]

A truly massive amount of work, I'm impressed. I'm glad we (well, you :-)) did this and CRefine is now as boring as it should be. You were right that this would have been extremely painful to do in CRefine (and multiple times for multiple queue types).

I only have cosmetic comments, the content looks very solid to me and it is much easier to follow than it would have been on the C level.

[michaelmcinerney]

I added a simp: argument to this little method, then removed it. And left behind these parentheses. I'll remove them.