|
|
|---|
|
|
|
|---|
G. D. Plotkin, “
The origins of structural operational semantics”, The Journal of
Logic and Algebraic Programming, 60 and 61, pp. 3-15, July
and December 2004.
Relevance: an interesting historical account of the
most popular (non-ACL2) approach to operational semantics
The term “structural Operational Semantics” was introduced by Gordon Plotkin in technical note DAIMI FN-19, Computer Science Department, Aarhus University, 1981. That sense of “operational semantics” is probably the most popular today and the literature has grown enormously since the original note. For that reason, we cite this “origins” paper because it was published in a two volume special issue of The Journal of Logic and Algebraic Programming. Furthermore, the original 1981 “Aarhus note” is included in that issue, and that special issue can be downloaded in full from this citation.
The approach to operational semantics most widely used in the ACL2 community is different from structural operational semantics. Plotkin formalized machines operationally but as inference rules (reminiscent of Hoare logic), whereas in ACL2 the logic is fixed — it is the logic of the ACL2 theorem prover — and in ACL2 the theory is extended via conservative definitions to describe the operation of the machines in question.
In this origins paper, Plotkin writes
“The IBM Vienna school [41,42] were interested in specifying real programming languages, and, in particular, worked on an abstract interpreting machine for PL/I using VDL, their Vienna Definition Language; they were influenced by the ideas of McCarthy, Landin and Elgot [18].
I remember attending a seminar at Edinburgh where the intricacies of their PL/I abstract machine were explained. The states of these machines are tuples of various kinds of complex trees and there is also a stack of environments; the transition rules involve much tree traversal to access syntactical control points, handle jumps, and to manage concurrency. I recall not much liking this way of doing operational semantics. It seemed far too complex, burying essential semantical ideas in masses of detail; further, the machine states were too big. The lesson I took from this was that abstract interpreting machines do not scale up well when used as a human-oriented method of specification for real languages (but see below for further comment).”
There is no doubt that interpretive operational semantics for commercial microprocessors is enormously complicated and much of that complexity is buried in data structures, but we in the ACL2 community tend to regard that as an unavoidable consequence of how the machines are designed and the fact that the structure of the designs manifest themselves in behaviors that users see. Would a structural operational semantics for the system-level view of x86 be less complex than the ACL2 x86 model described in bib::goel16? We also agree with Plotkin's observation that the interpretive approach does not scale well when used as a human-oriented method of specification for real languages. However, our focus is on mechanized reasoning about machines and we are optimistic that mechanization can manage the complexity. Furthermore, we believe the examples discussed in operational-semantics-2__other-examples support our optimism. Of course, as noted in operational-semantics-1__simple-example, the ACL2 user is responsible for configuring ACL2's prover to manage the complexity but the evidence is that expert users are capable of doing that, exploiting such ACL2 features as rewrite rules, metafunctions, enabling and disabling, pragmas for controlling rules, and hints (including computed hints).