sail-riscv
sail-riscv copied to clipboard
riscv
Note on software structure
I would like to suggest discussing an aspect of our Sail model's software structure.
Increasingly, some signatures are getting a bit complex to understand, e.g. [1]. This will get worse as we implement more extensions. The root cause of this is that we need to propagate information from a source (e.g. address translation or instruction decode) to a target (e.g. checks for memory RW rights). Let me call this, for lack of a better term, "trace-based incremental property checking".
What does that mean? As we execute the body of
function step(step_no : int) -> bool
we construct a lot of data, e.g. instruction bits, instruction AST, vaddr, paddr, PMAs etc. Later, using this data, we dispatch on what should be done, e.g. reservation, access fault etc. The important thing here is that we create the information earlier than we consume it. So the information has to be 'threaded-through' from producing site to consuming site. In other words we build up state. More precisely local state, since this information becomes invalid, when the instruction retires.
One way of looking at this is that we are, by hand, building (something akin to) a stack trace. There are several ways of handling such state.
-
Using the existing extension mechanism, e.g. the
ext_ptwin theTR_Resulttype. -
Stateful, add (non-architectural) registers for this.
-
Use different functions, e.g.
read_mem_plain,read_mem_giraffe,read_mem_dolphin, ... to track what instruction is doing the memory access -
Functional (essentially every function that is transitively called in step is getting an additional parameter tracking the state, which has type of a suitable struct)
Right now we have an uneasy hybrid of several of those.
I propose to consider instead defining a big struct, let's call it InstructionState, that carries all this information. When we want to add a new property that needs checking, we simply add a new field to InstructionState, add the relevant information where it is produced, and read it where it is consumed. At the start of each round of step we initialise the whole 'InstructionState' with each field being None().
The beauty of this is that whenever we add a new field we only have to edit only 3 places: definition of InstructionState, point were new information is produced and point where it is consumed. The whole call chain between consumer and producer of the new information remains unchanged. If we define a non-architectural register holding this information then we don't even have to add an additional place to all relevant functions to carry InstructionState, but in this case we have to worry about the state becoming inconsistent etc, in other words all the usual problems of maintaining state. More importantly: verification is typically much easier if you can 'see' what a function depends on simply by looking at the function signature.
Side note: the cognoscenti will know that we are talking about a state monad. This is not surprising since imperative state and the state monad are essentially equivalent. Be that as it may, Sail is (by design) not expressive enough to support monads. However it's worthwhile to be clear what we are doing. This also makes explanation easier.
[1] https://github.com/riscv/sail-riscv/blob/master/model/riscv_mem.sail#L179-L182
I think the memory code should be refactored to avoid passing three boolean arguments for release, acquire, and consistency. There are maybe some other parameters that could be grouped together into a memory operation struct of some sort. I'm not sure that logic applies to all instructions however.
I think a big struct can be problematic if it is ever the case that some of the fields are not meaningful, i.e. a struct only makes sense if all the fields make sense in all the places it is used (more or less). One problem we have encountered in the Arm spec translated into Sail, is that ASL has no tagged unions/variant types, so a lot of state is modelled as structs. Probably the most common bug we have encountered is some code A uses fields 1 and 2, whereas some other piece of code B uses fields 3 and 4. For code B fields 1 and 2 therefore need some kind of dummy values (we could use option types in natively written Sail, but ASL doesn't have those). The problem occurs when some update to the spec occurs and B now needs to use field 1, and since it's available in the struct it's easy... except it was never initialised so the code ends up using the dummy value without realising it. Essentially there ends up being a complex implicit invariant on the struct (a good example would be the FaultRecord type) which governs when certain fields are meaningful and this ends up making understanding the Arm spec much more difficult than it needs to be in my opinion.
@Alasdair That's very interesting. Some of the problems could be mitigated if some/all elements of the big struct were of type option(...) and default to None(), or some variation of that. Sail's tagged unions should be quite helpful.
Then it becomes a run time error, versus today where the static typing makes it a compile time error.
[adding Thibaut and Ben to cc]
Note that (eventually) some of this will probably have to change to propagate address translation info to support RISC-V virtual memory relaxed concurrency, in the same way and using the same ISA/concurrency interface as T&B have been considering for Arm.
Peter
On Wed, 3 Jan 2024 at 19:52, Martin Berger @.***> wrote:
I would like to suggest discussing an aspect of our Sail model's software structure.
Increasingly, some signatures are getting a bit complex to understand, e.g. [1]. The root cause of this is that we need to propagate information from a source (e.g. address translation or instruction decode) to a target (e.g. checks for memory RW rights). Let me call this, for lack of a better term, "trace-based incremental property checking".
What does that mean? As we execute the body of
function step(step_no : int) -> bool
we construct a lot of data, e.g. instruction bits, instruction AST, vaddr, paddr, PMAs etc. Later, using this data, we dispatch on what should be done, e.g. reservation, access fault etc. The important thing here is that we create the information later than we consume it. So the information has to be 'threaded-through' from producing site to consuming site. In other words we build up state. More precisely local state, since this information becomes invalid, when the instruction retires.
One way of looking at this is that we are, by hand, building (something akin to) a stack trace. There are several ways of handling such state.
Using the existing extension mechanism, e.g. the ext_ptw in the TR_Result type.
Stateful, add (non-architectural) registers for this.
Use different functions, e.g. read_mem_plain, read_mem_giraffe, read_mem_dolphin, ... to track what instruction is doing the memory access
Functional (essentially every function that is transitively called in step is getting an additional parameter tracking the state, which has type of a suitable struct)
Right now we have an uneasy hybrid of several of those.
I propose to consider instead defining a big struct, let's call it InstructionState, that carries all this information. When we want to check a new property, we simply add a new field to InstructionState, add the relevant information where it is produced, and read it where it is consumed. At the start of each round of step we initialise the whole 'InstructionState' with each field being None().
The beauty of this is that whenever we add a new field we only have to edit only 3 places: definition of InstructionState, point were new information is produced and point where it is consumed. The whole call chain between consumer and producer of the new information remains unchanged. If we define a non-architectural register holding this information then we don't even have to add an additional place to all relevant functions to carry InstructionState, but in this case we have to worry about the state becoming inconsistent etc, in other words all the usual problems of maintaining state. More importantly: verification is typically much easier if you can 'see' what a function depends on simply by looking at the function signature.
Side note: the cognoscenti will know that we are talking about a state monad. This is not surprising since imperative state and the state monad are essentially equivalent. Be that as it may, Sail is (by design) not expressive enough to support monads. However it's worthwhile to be clear what we are doing. This also makes explanation easier.
[1] https://github.com/riscv/sail-riscv/blob/master/model/riscv_mem.sail#L179-L182
— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/382, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFMZZRRC67OOMDEK7N27ZLYMWZIZAVCNFSM6AAAAABBL5FKPCVHI2DSMVQWIX3LMV43ASLTON2WKOZSGA3DINJWGY4DSMY . You are receiving this because you are subscribed to this thread.Message ID: @.***>
@PeterSewell That sounds interesting. Is this work already public, so we can have a look at it?
On further reflection, I doubt that the problem of specification evolution that @Alasdair points to is mitigated by the current RV model's profusion of parameters and functions. I imagine the problem remains (because it's a real problem) and just manifests itself differently. I also wonder if there might be an interesting PL research problem? The problem is that different spec versions need to gather and transmit information along different paths. So maybe a typing system that allows path dependencies but, paths are somehow parameterised by version, could be useful?
We could think about adding support for optional/named parameters or something to mitigate the profusion of parameters issue. The only problem I could imagine is that I don't think our theorem prover targets like Isabelle and Coq, which are where the general comprehensibility of the spec matters quite a bit support them.