Sporadic implies active #695

michaelmcinerney · 2023-11-07T09:07:11Z

Please see the commit messages for what's here.

Renamed, now that the invariant is more general. Signed-off-by: Michael McInerney <[email protected]>

lsf37 · 2023-11-07T21:29:16Z

proof/refine/ARM/Schedule_R.thy

+lemma sporadic_implies_active_cross:
+  "\<lbrakk>(s, s') \<in> state_relation; active_scs_valid s; sc_at scPtr s; ko_at' sc scPtr s';
+    scSporadic sc\<rbrakk>
+   \<Longrightarrow> is_active_sc' scPtr s'"


lsf37

This is great. And special thanks for the informative commit message :-)

lsf37 · 2023-11-07T21:38:26Z

proof/invariant-abstract/ARM/ArchDetSchedAux_AI.thy

+   \<lbrace>\<lambda>s. pred_map Q (sc_refill_cfgs_of s) p
        \<longrightarrow> pred_map (\<lambda>cfg. scrc_budget cfg = 0) (sc_refill_cfgs_of s) p\<rbrace>"


Not suggesting to change these, just out of curiosity: would it make sense to pull the implication into the pred_map? We don't seem to be doing this in other proofs either, but it looks shorter to me (and equivalent).

Yeah I think we could do that, and without too much of a change. Maybe it would make the lifting rules a little more annoying to deal with.

I'm definitely not suggesting changing anything at this point, but does us doing this for quite a few of our conditions indicate that we actually want finer-grained projections?

Oh when I saw Gerwin's comment, I thought he was referring to the statement of the new conjunct in active_scs_valid.

I didn't pay an awful lot of attention to these lemmas for retype_region etc. I think they're basically saying "if an active sched contexts exists after some deletion process occurred, then we didn't actually touch it" or "if we did retype it, it's now a default object". I am having a better look now to see if they can be improved or generalised.

@corlewis what sort of finger-grained projections were you thinking of? I think the sc_refill_cfgs_of projection works pretty well. It was used an awful lot for valid_refills

I did have a quick look to see whether it might be straightforward to get rid of the doubling up of pred_map in these sorts of implications. It's quite annoying, actually. I think these rules would work fairly well with hoare_vcg_imp_lift' or hoare_drop_imp, especially with the schematic predicates that are in some of these rules.

As for whether we should get rid of this sort of thing in the statement of the invariants, I would say that that would make sense, too. But I'm growing to rather dislike pred_map and its many often contorted variants. My vote would be to rewrite a lot of these invariants with opt_map in some way.

Should I leave all this as is for now?

Xaphiosis · 2023-11-08T04:47:51Z

proof/refine/RISCV64/Syscall_R.thy

+  "updateSchedContext scPtr (scBadge_update f) \<lbrace>invs'\<rbrace>"
+  apply (wpsimp wp: updateSchedContext_invs')
+  apply (intro conjI impI allI)
+    apply (erule (1) live_sc'_ko_ex_nonz_cap_to')


Is this erule very sensitive to things not being clarsimped before? Or maybe it's not in simp-normal form? Otherwise it looks tempting to give everything after the wpsimp to a fastforce. (similar temptation for scSporadic_update_invs'

I was able to compress this into one fastforce after the wpsimp in both proofs.

Xaphiosis · 2023-11-08T04:50:35Z

proof/invariant-abstract/DetSchedAux_AI.thy

@@ -665,11 +665,17 @@ lemma valid_sched_tcb_state_preservation_gen:
    "\<And>P. \<lbrace>\<lambda>s. (\<forall>p. pred_map active_scrc (sc_refill_cfgs_of s) p \<longrightarrow> pred_map P (sc_refill_cfgs_of s) p) \<and> I s\<rbrace>
            f \<lbrace>\<lambda>rv s. \<forall>p. pred_map active_scrc (sc_refill_cfgs_of s) p \<longrightarrow> pred_map P (sc_refill_cfgs_of s) p\<rbrace>"
  assumes sc_refill_cfg3:
-    "\<And>P. \<lbrace>\<lambda>s. (\<forall>p. pred_map (\<lambda>cfg. \<not> active_scrc cfg) (sc_refill_cfgs_of s) p
+    "\<lbrace>\<lambda>s. (\<forall>p. pred_map (\<lambda>cfg. \<not> active_scrc cfg) (sc_refill_cfgs_of s) p


maybe I'm confused by the diff, but is the implication on the next line now incorrectly indented?

Ah, this was incorrect. Fixed, thanks

Xaphiosis · 2023-11-08T04:57:12Z

spec/haskell/src/SEL4/Object/SchedContext.lhs

@@ -525,6 +525,7 @@ This module uses the C preprocessor to select a target architecture.
 > schedContextZeroRefillMax :: PPtr SchedContext -> Kernel ()
 > schedContextZeroRefillMax scPtr = do
 >     updateSchedContext scPtr $ (\sc -> sc { scRefillMax = 0 })
+>     updateSchedContext scPtr $ (\sc -> sc { scSporadic = False })


This is a bit odd, we now have schedContextZeroRefillMax setting scSporadic, which minimises turbulence in the rest of the proof, but doesn't seem to make a lot of sense to read. This file is a bit sparse on commentary, which doesn't make it easier to grasp the meaning for the uninitiated.

This function has drifted over the last few years, so the name is no longer a good one. This function is now probably better thought of as zeroing (in a general sense) all of the fields for the "sporadic" parts of the sched context. But I'm not really sure what "sporadic" means any more...

Would it be better to call it sched_context_zero_sporadic_fields or something? I can't think of anything better

Yeah, your comment and the better name makes more sense (I'm guessing you'd want a camelCase name since this is Haskell). If it's inconvenient to do in this PR, can maybe add a rename to another day, but the helpful comment would still be welcome.

Actually, maybe sched_context_zero_sporadic_fields isn't such a good name: presumably we could have the sc_sporadic field be False, so that sched context isn't "sporadic", but we'd still like to call this function to make the sc inactive. So it really does seems like it makes it inactive (which is why it was called zero_refill_max to begin with) and then we've just got a bunch of other things we'd like to zero out in order to keep the invariants happy. Still not sure what to call it, then.

I think it should be renamed, but considering that the name was off before this work was started, it would be better to redo the naming in another PR.

And yes, camelCase for the Haskell, but we do have the analogue of this function in the abstract spec as well.

I think making it inactive is the right view -- that requires resetting the refills and the sporadic flag at the same time, because it's not properly inactive if the sporadic flag is still set.

Xaphiosis · 2023-11-08T04:58:59Z

Nice work, this looks like an improvement, and the commit messages are more informative than the comments in the specs, thus helping a lot with understanding what you did in this PR!

This adds an invariant to active_scs_valid (part of valid_sched) which states that every scheduling context which is sporadic is active. Several changes to the specs were made, in particular - a sched context is made not sporadic during the finalisation process. This was required to prove the invariant holds. - the update to the sc_sporadic field within invoke_sched_control_configure_flags is now made towards the end of the function, so as to ensure that the field is updated only after the scheduling context is made active. This means that the new invariant is not broken temporarily, and eases the proofs. In addition, the update to the sc_badge field is moved. - if_cond_refill_unblock_check is modified, taking into account the new invariant. Signed-off-by: Michael McInerney <[email protected]>

This renames sched_context_zero_refill_max to sched_context_set_inactive, now that the function does more. A similar rename has been done for the Haskell too. Signed-off-by: Michael McInerney <[email protected]>

rt proof: rename active_sc_valid_refills to active_scs_valid

468a7e4

Renamed, now that the invariant is more general. Signed-off-by: Michael McInerney <[email protected]>

michaelmcinerney added the MCS related to `rt` branch and mixed-criticality systems label Nov 7, 2023

michaelmcinerney requested review from Xaphiosis, lsf37 and corlewis November 7, 2023 09:07

michaelmcinerney self-assigned this Nov 7, 2023

michaelmcinerney force-pushed the michaelm-sporadic_imp_active branch from 719c755 to ea860f5 Compare November 7, 2023 14:03

lsf37 reviewed Nov 7, 2023

View reviewed changes

lsf37 approved these changes Nov 7, 2023

View reviewed changes

lsf37 reviewed Nov 7, 2023

View reviewed changes

Xaphiosis reviewed Nov 8, 2023

View reviewed changes

Xaphiosis approved these changes Nov 8, 2023

View reviewed changes

michaelmcinerney added 2 commits November 9, 2023 14:14

rt spec: rename sched_context_zero_refill_max

60c79a4

This renames sched_context_zero_refill_max to sched_context_set_inactive, now that the function does more. A similar rename has been done for the Haskell too. Signed-off-by: Michael McInerney <[email protected]>

michaelmcinerney force-pushed the michaelm-sporadic_imp_active branch from ea860f5 to 60c79a4 Compare November 9, 2023 03:45

michaelmcinerney merged commit 9b4c436 into rt Nov 9, 2023
11 checks passed

michaelmcinerney deleted the michaelm-sporadic_imp_active branch November 9, 2023 10:51

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Sporadic implies active #695

Sporadic implies active #695

michaelmcinerney commented Nov 7, 2023

lsf37 Nov 7, 2023

lsf37 left a comment

lsf37 Nov 7, 2023

michaelmcinerney Nov 7, 2023

corlewis Nov 8, 2023

michaelmcinerney Nov 8, 2023

michaelmcinerney Nov 8, 2023

Xaphiosis Nov 8, 2023

michaelmcinerney Nov 9, 2023

Xaphiosis Nov 8, 2023

michaelmcinerney Nov 8, 2023

Xaphiosis Nov 8, 2023

michaelmcinerney Nov 8, 2023 •

edited

Loading

Xaphiosis Nov 8, 2023

michaelmcinerney Nov 8, 2023

lsf37 Nov 8, 2023

Xaphiosis commented Nov 8, 2023

		\<lbrace>\<lambda>s. pred_map Q (sc_refill_cfgs_of s) p
		\<longrightarrow> pred_map (\<lambda>cfg. scrc_budget cfg = 0) (sc_refill_cfgs_of s) p\<rbrace>"

Sporadic implies active #695

Sporadic implies active #695

Conversation

michaelmcinerney commented Nov 7, 2023

Choose a reason for hiding this comment

lsf37 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

michaelmcinerney Nov 8, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Xaphiosis commented Nov 8, 2023

michaelmcinerney Nov 8, 2023 •

edited

Loading