adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

refine: comments for pspace_storable 

We keep on forgetting what the parameters to loadObject and storeObject
mean, and why we have pspace_storable in the first place. Hopefully
these comments mean having to re-remember fewer things.

Signed-off-by: Edward Pierzchalski <ed.pierzchalski@data61.csiro.au>
This commit is contained in:
Edward Pierzchalski 2020-05-06 22:04:55 +10:00 committed by Gerwin Klein
parent bd4392d132
commit 7c6b2af816
1 changed files with 120 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

120
spec/design/skel/PSpaceStorable_H.thy
View File

@ -114,9 +114,129 @@ end
class pspace_storable = pre_storable +
fixes makeObject :: 'a
\<comment>\<open>
`loadObject` is only used in the generic definition of `getObject`. It
describes how to extract a value of type `'a` from memory.
If `(obj, _) \<in> loadObjext p before after ko` within `getObject`, then:
- @{term "p :: machine_word"} is the addres that we want to read an
instance of `'a` from.
- @{term "before :: machine_word"} is the address of the nearest
object at or before `p`.
- @{term "after :: machine_word option"} is the address of the nearest
object after `p`, if any (for checking overlap).
- @{term "ko :: kernel_object"} is the object currently at `before`.
- @{term "obj :: 'a"} is the value extracted from `ko`.
Graphically, the "memory" looks like this:
before p after
|-------|--+-----+-----|---|
| +~~+ <---+---------- The span of obj, the object we want to extract.
+~~~~~~~~~~~~~~~~+ <-------- The span of ko, the existing object that spans obj.
+~~~+ The span of whatever object comes after obj.
We don't care about this beyond making sure
it doesn't overlap with ko.
In almost every case, the object in memory (ko) is the same type of object
as the one being loaded (obj). For example, for a reply object our parameters
look like this:
p, before
|-----------|
+~~~~~~~~~~~+ <- The span of two objects:
- ko, the existing object (which should be a reply object).
- obj, the object that we want to load from memory. This will
just be ko projected through @{term projectKO}.
In these simple cases, @{term loadObject_default} is a good specification
for how to load an instance of `'a` from memory.
The only interesting case is when we're loading a CTE, which might be
inside a TCB. Then memory looks like this:
before p
|-------|--+-----+
| +~~+ <---+---- The span of obj, i.e. the CTE which we're reading from
| | memory.
+~~~~~~~~~~~~~~~~+ <-- The span of ko, i.e. the TCB surrounding and containing
obj.
In this case, the process for extracting the CTE from the surrounding TCB
is more involved. See `loadObject_cte` in `ObjectInstances_H`.
\<close>
fixes loadObject :: "machine_word \<Rightarrow> machine_word \<Rightarrow> machine_word option \<Rightarrow> kernel_object \<Rightarrow> 'a kernel"
\<comment>\<open>
`updateObject` is only used in the generic definition of `setObject`,
but it shows up in a few lemma statements as well. It describes how to update
the kernel object contents of memory depending on what's already in that
memory.
If `(ko', _) \<in> updateObject v ko p before after s` within `setObject`, then:
- @{term "v :: 'a"} is the new object you want to write at pointer
@{term "p :: machine_word"}.
- @{term "before :: machine_word"} is the address of the nearest
object at or before `p`.
- @{term "ko :: kernel_object"} is the object currently at `before`.
- @{term "after :: machine_word option"} should be the address of the nearest
object after `p`, if any (for checking overlap).
- The returned value @{term "ko' :: kernel_object"} is the old object `ko`,
updated as required by `v`. This value gets inserted by `setObject` into
memory at the address `before`.
Graphically, the "memory" looks like this:
before p after
|-------|--+-----+-----|---|
| +~~+ <---+---------- The span of v, the object we want to insert.
+~~~~~~~~~~~~~~~~+ <-------- The span of ko, the existing object that spans v.
This is also the span of ko', which will be what
gets put into memory after the update.
+~~~+ The span of whatever object comes after ko.
We don't care about this beyond making sure
it doesn't overlap with ko before or after it
gets updated with v.
In almost every case, the object in memory (ko) is the same type of object
as the one being inserted (v). For example, for a reply object our parameters
look like this:
p, before
|-----------|
+~~~~~~~~~~~+ <- The span of three objects:
- v, the new reply object we want to insert.
- ko, the existing object (which should be a reply object).
- ko', the new object (which should be a reply object if
the previous one was).
In these simple cases, @{term updateObject_default} is a good specification
for how to update the existing kernel object.
The only interesting case is when we're updating a CTE, which might be
inside a TCB. Then memory looks like this:
before p
|-------|--+-----+
| +~~+ <---+---- The span of v, i.e. the CTE which we're inserting into
| | memory.
+~~~~~~~~~~~~~~~~+ <-- The span of ko, i.e. the TCB surrounding and containing v.
This is also the span of ko', which is "just" a copy
of ko with the relevant CTE updated.
In this case, the process for updating the surrounding TCB is more involved.
See `updateObject_cte` in `ObjectInstances_H`.
\<close>
fixes updateObject :: "'a \<Rightarrow> kernel_object \<Rightarrow> machine_word \<Rightarrow> machine_word \<Rightarrow>
machine_word option \<Rightarrow> kernel_object kernel"
\<comment>\<open>
If updating an object succeeds, then the type of the updated object (ko')
should be the same as the original object (ko).
\<close>
assumes updateObject_type:
"(ko', s') \<in> fst (updateObject v ko p p' p'' s) \<Longrightarrow> koTypeOf ko' = koTypeOf ko"