From 7c6b2af816a0f9de3e96ce2c7d475837a183e85c Mon Sep 17 00:00:00 2001 From: Edward Pierzchalski Date: Wed, 6 May 2020 22:04:55 +1000 Subject: [PATCH] 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 --- spec/design/skel/PSpaceStorable_H.thy | 120 ++++++++++++++++++++++++++ 1 file changed, 120 insertions(+) diff --git a/spec/design/skel/PSpaceStorable_H.thy b/spec/design/skel/PSpaceStorable_H.thy index f36c7f065..8915cc419 100644 --- a/spec/design/skel/PSpaceStorable_H.thy +++ b/spec/design/skel/PSpaceStorable_H.thy @@ -114,9 +114,129 @@ end class pspace_storable = pre_storable + fixes makeObject :: 'a + + \\ + `loadObject` is only used in the generic definition of `getObject`. It + describes how to extract a value of type `'a` from memory. + + If `(obj, _) \ 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`. + \ fixes loadObject :: "machine_word \ machine_word \ machine_word option \ kernel_object \ 'a kernel" + + \\ + `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', _) \ 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`. + \ fixes updateObject :: "'a \ kernel_object \ machine_word \ machine_word \ machine_word option \ kernel_object kernel" + + \\ + If updating an object succeeds, then the type of the updated object (ko') + should be the same as the original object (ko). + \ assumes updateObject_type: "(ko', s') \ fst (updateObject v ko p p' p'' s) \ koTypeOf ko' = koTypeOf ko"