As we know, there are multiple style of program semantics: operational, axiomatic, denotational, etc. I’m wondering if data_type forms its own kind of semantics for the programs that it represents. Let me expand.
In the refinement proof, data_type is the core abstraction that represents processes, and each data_type (i.e. for the abstract spec, executable spec, and C-implementation) is arrived at by different means. By this I mean, the abstract spec is written in a monadic style, whereas the C-implementation is obviously written in C. Both styles have to be mapped to a data_type to be compared.
In the C example, the data_type is implemented via the SIMPL operational semantics of the parsed C code. Does this mean that data_type is just an alternative semantics of the C code? Is semantics the right lens to be looking at data_type through?
It almost seems to me like data_type is more of a denotational semantics, but the mechanism of constructing a data_type for each process is not one that I’ve seen in any literature about semantics, so I’m just wondering if that’s the correct way to think about it.
That depends on what you mean by data_type. Do you mean an abstract data type in the form we use for refinement in the seL4 verification, i.e. the one defined in theory Simulation?
We mainly use these as a general very abstract framework that we can easily cast the other different semantic styles into, because it basically views the system one gigantic state machine and abstracts from details like data representation, rules, etc. It makes no assumptions about being used for a programming language or for a specific system, it just talks about executions and has enough detail to formulate once what we want data refinement to mean. That means, it gives us one central definition of refinement that we can then use to justify the more specific and sometimes more complex properties we prove about monads or C or other constructs.
I guess some people do use such abstract automata frameworks (I’m not sure any more actually why the literature calls them data types) directly for specifying the semantics of languages or systems, so in that sense, yes, they are another semantic style. Then again, Turing machines or lambda calculus would also be such semantic styles, the question is how convenient/powerful they are to describe the kind of programming language or system under consideration.
For us, they are a mechanism to unify the different semantic styles we use into one final theorem so that the different styles compose nicely.
Yea, I meant the data_type definition in the Simulation theory (it’s called process in the refinement papers).
because it basically views the system one gigantic state machine and abstracts from details like data representation, rules, etc.
That’s exactly what made me think of this - a very similar definition (state transition system) is what powers the semantics TLA+ for example. I was wondering if saying “denotational semantics” for this is accurate (the denotation of the syntax is the manipulation of the state transition system).
I get the general idea, I’m just hung up on the actual terminology a bit. And maybe that’s not even so important. The data_type definition can represent program semantics, one way or the other.
Yes, such state machines are used a lot as basic computation model, and ADTs can definitely represent program semantics.
I would still say denotational semantics is something different. A denotation usually is a function that goes from a syntactic construct to a semantic domain, and an ADT is not that function.
An example for syntactic constructs would be assignment, if/then/else, while, and an example for a semantic domain would be partial functions between states (building such partial functions compositionally if you have while in the language is a bit tricky, and tends to lead down the track to domain theory, fixed points, the logic of computable functions, etc.). Compositionally here would mean that if [[ f ]] stands for the “the semantics of the syntactic construct f”, then you’d build [[ f; g ]] out of [[f]] and [[g]] (for ; this is still easy, it’s usually just [[g]] o [[f]]). For ADTs you don’t necessarily get compositionality so easily, i.e. to compose them you usually do point-wise constructions, hooking up transitions or final/start states with each other, whereas denotational semantics tend to map things to operators, i.e. ; to o or while to fix-point operator, etc.
That’s not to say that ADTs don’t in the end give you the same laws for reasoning about programs, i.e. you can still reason about them compositionally, but the construction, and the feel and purpose of a denotational semantics would be a bit different.
I would call the semantics of TLA+, as well as the semantics for most other system description languages from the model checking area, but also the semantics we eventually use for our refinement a “state-machine semantics” or “state-machine based semantics”.
That’s right, I forgot about the composition requirement of denotational semantics. Thanks for clarifying. Whatever the name is, I enjoy the state-machine semantics very much, because of its simplicity.
The main missing piece for me was the “correspondence” framework in the sel4 proof. This is what maps the language-specific programs to ADTs. I never fully understood the correspondence step, but now it makes a lot more sense - there needs to be a way to go from both non-deterministic monad specs and C programs to ADTs.
The crucial distinction here is between the mathematical objects (ADTs) and the definitional mechanism by which they are associated with syntactic objects (programs). ADTs have just enough structure to represent relevant semantic properties of the programs involved in the seL4 chain of proofs so far.
This is no longer the case for these ADTs when one becomes interested in concurrency (ADTs lack abstract notions of fairness etc.) or most aspects of security (e.g. absence of side channels).
I’ve also wondered this - if we can map a spec written with non-determinism (e.g. using the non-deterministic monad type) to ADTs, then why isn’t that enough to handle concurrency? I know there are other models of concurrency, but I thought that non-deterministic state transitions were enough to model it as well.
Non-determinism can be good enough to model concurrency if all one cares about are safety properties. Termination and other liveness properties can suffer because plain non-determinism does not fully incorporate the usual requirement of
The execution speed of every non-terminated and non-deadlocked process is positive and arbitrary, unless it is waiting for access to a shared variable, in which case, by waiting long enough, access is eventually granted and the process resumes execution.