numdomains: make proofs work with any number of domains #410

Xaphiosis · 2021-12-20T23:55:01Z

This is still limited to 256 domains because domain type is word 8 and quite hardcoded in the abstract specs/proofs. Please see commit messages for detailed observations on how this was accomplished, and caveats.

The default regression test will check with numDomains=16, and I've been running tests with numDomains=1 which was the most difficult to deal with due to "clever" simplification of edge cases spat out via ArrayGuards.

lsf37 · 2021-12-21T00:14:22Z

Not sure what ails the link checker today, but it has been failing on all repos this morning, so is unrelated to this PR. Some "503 Service unavailable" thing at docker.

The theory linter fail is anticipated, the interactive commands are for demonstrating the features of the command.

lsf37 · 2021-12-21T01:52:24Z

Not sure what ails the link checker today, but it has been failing on all repos this morning, so is unrelated to this PR. Some "503 Service unavailable" thing at docker.

There is now an actual link check failure, which is unrelated. Fix is in #412

Xaphiosis · 2021-12-21T03:58:26Z

Found a hiccup when numDomains=2 and simplification of 0 < 1, force-pushed the change. Running tests with numDomains=17 as well to make sure I haven't missed anything.

Xaphiosis · 2021-12-21T05:02:58Z

In case this looks PR looks quiet, @lsf37 reviewed this twice already

lib/Value_Type.thy

corlewis · 2021-12-21T06:11:05Z

lib/Value_Type.thy

+(* Remove the demo definitions: *)
+hide_const num_domains
+hide_fact num_domains_def
+
+hide_const num_prio
+hide_fact num_prio_def


I don't think that this completely removes the definitions. From memory, it makes them very hard to access but they can still turn up unexpectedly in find_theorems and find_consts.

It's probably unlikely to cause any actual issues, but my preference is to put these examples in a separate file that isn't imported.

I had suspected something like this. Thoughts, @lsf37 ?

Yeah, @corlewis is right, we should put this in a separate theory. I had hoped to be able to pull the definitions into the experiment block, but while the definitions do work there, the code generator seems to refuse to generate anything for them inside the local context, which means that eval won't work.

In more detail: eval complains that there are not code equations for num_domains in the example if you move the definition into the local context, but if you try and explicit export_code it will already complain that there is no constant num_domains. This does make some sense, because if there are assumptions or fixed variables in the context the generated code will not have the right semantics.

All this means this is a limitation of the value_type command in general: it can't use terms on the rhs that are only defined in a local context. If we ever need that, we'll need to use something else to compute the numeral.

I'll add a comment to that effect and move the example into a separate theory.

corlewis · 2021-12-21T06:34:47Z

proof/invariant-abstract/ARM/ArchDetSchedDomainTime_AI.thy

+               (* unless we hit dec_domain_time we know ?dtnot0 holds on the state, so clean up the
+                  postcondition once we hit thread_set_time_slice *)
+               hoare_post_imp[where Q="\<lambda>_. ?dtnot0" and R="\<lambda>_ s. domain_time s = 0 \<longrightarrow> X s"
+                                and a="thread_set_time_slice t ts" for X t ts]
+               hoare_drop_imp[where f="ethread_get t f" for t f])


This is a nice way of handling this (and a very useful comment)!

This might be a whitespace change, reindent or moving things around, don't think I did anything this round on it, though I did possibly write the original.

corlewis · 2021-12-21T06:39:45Z

proof/infoflow/ADT_IF.thy

@@ -1502,7 +1502,6 @@ locale valid_initial_state_noenabled = invariant_over_ADT_if + (* FIXME: arch_sp
  assumes scheduler_action_s0_internal: "scheduler_action s0_internal = resume_cur_thread"
  assumes ct_running_or_ct_idle_s0_internal: "ct_running s0_internal \<or> ct_idle s0_internal"
  assumes domain_time_s0_internal: "domain_time s0_internal > 0"
-  assumes num_domains_sanity: "num_domains > 1"


Wow, great job removing this! I thought that there being multiple domains was a pretty important condition for infoflow.

It is if you want an interesting state, you'll see when you get to InfoflowC changes to ExampleValidStateH

corlewis · 2021-12-21T07:21:37Z

proof/refine/ARM/Schedule_R.thy

+lemma invs_no_cicd_ksCurDomain_maxDomain':
+  "invs_no_cicd' s \<Longrightarrow> ksCurDomain s \<le> maxDomain"


nitpick: move this to Invariants_H and make it elim! like the similar rules (same for other architectures)

Can you elaborate which similar rules you are thinking of? I'm not seeing any invs_no_cicd' derivations in Invariants_H. Happy to put it there, but would like more clarity of the idea. invs_no_cicd'_queues also lives in Schedule_R and probably was the same low level of inspiration.

I was considering it as similar to rules like invs_valid_objs'. There's no big problem with leaving it as is, especially if invs_no_cicd'_queues is already there as well, but everything else being equal I do like having this sort of lemma early in the dependencies.

proof/refine/ARM/Schedule_R.thy

corlewis

This all looks great to me. It's really nice to see this progress towards more automatically supporting different configurations!

With regards to the crefine work, I mainly looked at the ARM changes along with skimming the RISCV64 files. I assume that the others are similar.

corlewis · 2021-12-22T00:49:20Z

proof/crefine/ARM/Wellformed_C.thy

+lemma num_tcb_queues_calculation: "num_tcb_queues = numDomains * numPriorities"
+  unfolding num_tcb_queues_def by eval


I'm not sure what the point of this lemma is. Is it confirming that the constant created by the value_type is correct?

Not quite. Let's assume 16 domains and 256 prios. Then the value_type generates a definition that says "num_tcb_queues = 4096" and a type abbreviation "num_tcb_queues" that's also 4096, with a loss of info for how that calculation took place. So for example, in the proof of cready_queues_index_to_C_in_range' I don't unfold numDomains_def or numPriorities_def even though you would expect me to normally. The outcome is still a lemma that says something like _ < 4096 but we don't have to unfold the reasons for why it's 4096. It is a bit circular, like trying to not step on one's own toes, and probably not the high point of the abstraction. Does this help at all?

Right, that makes sense. The bit I was missing is that how the calculation occurred was useful in other lemmas. With that in mind, I can't think of a nicer way to handle it than what you've done.

corlewis · 2021-12-22T01:33:08Z

proof/crefine/ARM/Invoke_C.thy

  apply (clarsimp simp: valid_tcb_state'_def invs_valid_queues' invs_valid_objs'
                        invs_queues invs_sch_act_wf' ct_in_state'_def pred_tcb_at'
                        rf_sr_ksCurThread word_sle_def word_sless_def sysargs_rel_to_n
                        mask_eq_iff_w2p mask_eq_iff_w2p word_size "StrictC'_thread_state_defs"
-                        maxDomain_def numDomains_def)
+                        )


tiny nitpick: remove newline before the closing parenthesis

corlewis · 2021-12-22T01:34:57Z

proof/crefine/ARM/IpcCancel_C.thy

+  (* 256 looks like numPriorities *)
  apply (auto simp: cready_queues_index_to_C_def numPriorities_def
                    seL4_MaxPrio_def word_le_nat_alt dest: arg_cong[where f="\<lambda>x. x mod 256"])


Is this comment intended to still be here? I guess the fact that you didn't need to replace the number means that it isn't representing numPriorities?

You mean numDomains? I was worried the 256 had to do with 2 ^ LENGTH(8) where 8 is the size in bits of the domain type, but there also happen to be 256 numPriorities. I still suspect it's the latter, but probably safe even if it's the former. I'll drop the comment.

Ah ok, I was reading the comment the other way around, more as a FIXME. I thought you meant that 256 might be numPriorities, and that if it was you would want to replace it.

proof/crefine/ARM/IpcCancel_C.thy

corlewis · 2021-12-22T01:37:29Z

proof/crefine/ARM/IpcCancel_C.thy

+  apply (clarsimp simp: word_size prioToL1Index_def wordRadix_def mask_def
+                        invertL1Index_def l2BitmapSize_def'
+                        le_maxDomain_eq_less_numDomains word_le_nat_alt)
+  apply (case_tac "da = d" ; clarsimp simp: num_domains_index_updates)


Maybe rename the da first?

I can take a look. This is copied/moved, so I don't know where da is in the order for renaming. Still, good suggestion.

investigate da rename

Fixed this one, it was indeed unnecessary. For the other ones it makes little difference to rename, it's just another d so all we could rename it to is d'.

corlewis · 2021-12-22T02:07:18Z

proof/crefine/ARM/Wellformed_C.thy

+  unfolding Kernel_C.maxDom_def maxDomain_def Kernel_Config.numDomains_def
+  by clarsimp
+
+lemma num_domains_calculation: "num_domains = numDomains"


Suggested change

lemma num_domains_calculation: "num_domains = numDomains"

lemma num_domains_calculation:

"num_domains = numDomains"

lib/Value_Type.thy

lib/test/Value_Type_Test.thy

The `value_type` top-level command allows evaluating a term down to a natural number, and using that number to define an enumerated type, as well as (optionally) a constant definition. Co-authored-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems> Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Introduce Kernel_Config theory for storage of non-architecture-specific seL4 configuration variables that are shared by the abstract and design specs. Remove `num_domains`, in lieu of `numDomains` that is now defined only in `Kernel_Config.thy`. The definition is hidden and must be referred to as Kernel_Config.numDomains_def when avoiding unfolding is not possible. Include required properties of `numDomains` as lemmas. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Make proofs work with any number of domains that fits in the domain type (at this time an 8-bit word). Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

The proofs work without knowing the number of domains, including with only a single domain. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Proofs now don't care about numDomains, except for a small interface in Invariants_H. The interface is currently by convention only, and has no enforcement capabilities. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

For CRefine, this process is much more complex than for Refine and up, as the C code both has its own definitions `maxDom` and `numDomains`, but they are not defined in terms of each other, only numbers. Similarly, array size types and their corresponding ArrayGuard bounds checks refer to specific numbers, making a fullproof abstraction impossible. A reasonably constrained interface to numDomains/maxDomain/maxDom in Wellformed_C provides a sufficient abstraction to allow the proofs to be independent of the number of domains (constrained to <= 256). Using the value_type command allows more abstraction techniques, such as linking the size of the scheduler queues back to numDomains*numPriorities, without stating what the numbers are. Finally, for getting past the ArrayGuard bounds checks, we do leak some information in the form of `explicit` lemmas. These are the least safe, but short of augmenting the C parser to re-wrap array sizes into equivalent constants/types, they constitute a limited risk. Nonetheless, `explicit` lemmas should be used as sparingly as possible. Refinement to C proceeds by pretending we don't know the number of domains, and whenever a control flow decision is made based on `numDomains > 1`, we follow both branches, as we did for Refine. We also attempt to avoid clever rewrites such as `(x < 1) = (x = 0)` which mess up bounds checks into a domain-size array when `numDomains = 1`. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

The InfoFlow proof itself does not care about the number of domains, and that assumption was removed in another commit. The specific example in the information flow refinement requires two domains (one "high" and one "low") to be of any interest. Since it cannot be instantiated with only one domain, the example theorems in Example_Valid_StateH now assume that `1 <= maxDomain`. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Xaphiosis · 2021-12-22T05:24:46Z

All @corlewis issues should be addressed now. Squashed and rebased, ready to merge once tests pass to make sure I didn't mess up anything by mistake.

Xaphiosis requested review from lsf37 and corlewis December 20, 2021 23:55

lsf37 approved these changes Dec 21, 2021

View reviewed changes

lsf37 mentioned this pull request Dec 21, 2021

abs-config: lift ASpec+ExecSpec config values from C config #411

Merged

Xaphiosis force-pushed the numdomains branch from 73d6608 to 49f092a Compare December 21, 2021 03:56

lsf37 mentioned this pull request Dec 21, 2021

add CI for different numDomains settings #413

Closed

corlewis reviewed Dec 21, 2021

View reviewed changes

corlewis approved these changes Dec 22, 2021

View reviewed changes

corlewis reviewed Dec 22, 2021

View reviewed changes

lib/Value_Type.thy Outdated Show resolved Hide resolved

corlewis reviewed Dec 22, 2021

View reviewed changes

lib/test/Value_Type_Test.thy Outdated Show resolved Hide resolved

lsf37 and others added 7 commits December 22, 2021 16:20

ainvs: update proofs to never unfold numDomains

5847a2c

Make proofs work with any number of domains that fits in the domain type (at this time an 8-bit word). Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

infoflow: remove dependency on domains > 1

13634c9

The proofs work without knowing the number of domains, including with only a single domain. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

Xaphiosis force-pushed the numdomains branch from 60b2b69 to f27f261 Compare December 22, 2021 05:21

Xaphiosis mentioned this pull request Dec 22, 2021

Add numDomains enumeration constant seL4/seL4#713

Merged

lsf37 added the enhancement label Dec 22, 2021

Xaphiosis merged commit 73911da into master Dec 22, 2021

Xaphiosis deleted the numdomains branch December 22, 2021 12:50

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

numdomains: make proofs work with any number of domains #410

numdomains: make proofs work with any number of domains #410

Xaphiosis commented Dec 20, 2021

lsf37 commented Dec 21, 2021

lsf37 commented Dec 21, 2021

Xaphiosis commented Dec 21, 2021

Xaphiosis commented Dec 21, 2021

corlewis Dec 21, 2021

Xaphiosis Dec 21, 2021

lsf37 Dec 21, 2021

corlewis Dec 21, 2021

Xaphiosis Dec 21, 2021

corlewis Dec 21, 2021

Xaphiosis Dec 21, 2021

corlewis Dec 21, 2021

Xaphiosis Dec 21, 2021

corlewis Dec 21, 2021

corlewis left a comment

corlewis Dec 22, 2021

Xaphiosis Dec 22, 2021

corlewis Dec 22, 2021

corlewis Dec 22, 2021

Xaphiosis Dec 22, 2021

corlewis Dec 22, 2021

Xaphiosis Dec 22, 2021

corlewis Dec 22, 2021

corlewis Dec 22, 2021

Xaphiosis Dec 22, 2021 •

edited

Loading

Xaphiosis Dec 22, 2021

corlewis Dec 22, 2021

Xaphiosis Dec 22, 2021

Xaphiosis commented Dec 22, 2021

		lemma invs_no_cicd_ksCurDomain_maxDomain':
		"invs_no_cicd' s \<Longrightarrow> ksCurDomain s \<le> maxDomain"

		lemma num_tcb_queues_calculation: "num_tcb_queues = numDomains * numPriorities"
		unfolding num_tcb_queues_def by eval

	lemma num_domains_calculation: "num_domains = numDomains"
	lemma num_domains_calculation:
	"num_domains = numDomains"

numdomains: make proofs work with any number of domains #410

numdomains: make proofs work with any number of domains #410

Conversation

Xaphiosis commented Dec 20, 2021

lsf37 commented Dec 21, 2021

lsf37 commented Dec 21, 2021

Xaphiosis commented Dec 21, 2021

Xaphiosis commented Dec 21, 2021

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

corlewis 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

Xaphiosis Dec 22, 2021 • 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 Dec 22, 2021

Xaphiosis Dec 22, 2021 •

edited

Loading