The Zarf ISA Static Semantics

Preview

Michael presented the static semantics of the Zarf ISA, as found in this document, which is being partially included in the pending typed binary submission for ISCA 2018.

Summary

Zarf is a novel, purely functional ISA. As originally designed, it is control-flow and memory safe, and the ISA presented greatly simplifies formal reasoning about its properties. However, this does not preclude the occurences of all hardware errors, such as improper arguments being passed to a function call or trying to scrutinize a non-value. In all invalid cases, the system returns an error object that can be pattern-matched on and handled by any function. With such a simple machine, one which already resembles the lambda calculus, the majority of these errors can be easily avoided if the machine is typed.

Typed Zarf adds types directly into the binary, such that a hardware typechecker can now verify that any program is well-typed. The following changes were needed to make Zarf typed: - All constructors must now be members of a datatype (similar to algebraic data types in Haskell and ML) - All case instructions must be complete (all the constructor patterns for the scrutinized datatype must be present, otherwise an else branch must be present) - Functions must be annotated with their parameter and return types. - The machine now recognizes and can track the following types: int, function, user-defined datatype, and type variable.

With the support for type variables, all datatypes and functions can be made polymorphic. The original Zarf instructions (let, case, and result) remain the same (i.e. no type annotations are present in a function’s instructions), such that type checking requires local type inference. The machine uses standard unification and substitution to get the principal type of each variable defined in a let instruction as well as to determine equality of case branches and result types. The typechecker has been formalized in the document linked in the preview; a Prolog implementation of the specification is used for test generation, and a Haskell implementation is used as an oracle for comparing the measuring the correctness of the hardware implementation. More importantly, these typing rules have been designed such that they can be (and indeed have been) implemented with a state machine in hardware.

Discussion

We went over the metalanguage of inference rules for those unfamiliar with them. Michael explained some of the subtle details of the static semantics, including the use of rigid vs. generic type variables, and gave an example where the distinction is useful during unification. We discussed the case-con rule and its associated helper functions to get a feel for what the system is doing. Michael also explained how applyType works (which is the heart of the unification and substitution algorithm), and how it handles recursive-lets properly. The group also gave suggestions on how to improve the presentation of some of the rules and some various symbol usage. Finally, we briefly went through some figures in the pending ISCA 2018 submission, mentioning the graphs on machine state coverage and the binary translation.