Processor architectures are critical interfaces in computing, but they are
typically defined only by prose and pseudocode documentation. This is
especially problematic for the subtle concurrency behaviour of weakly
consistent multiprocessors such as ARM and IBM POWER: the traditional
documentation does not define precisely what programmer-observable behaviour is
(and is not) allowed for concurrent code; it is not executable as a test oracle
for pre-Silicon or post-Silicon hardware testing; it is not executable as an
emulator for software testing; and it is not mathematically rigorous enough to
serve as a foundation for software verification. In order to rigorously specify
architectures, the instructions, pipelines, and memory controllers must be
specified using formally defined languages and and tools.

In this talk, I will present my domain specific language, Sail, for specifying
architecture instructions sets. The resulting specifications form one part of
rigorous architectural models for POWER and ARM. I will present the interesting
aspects of Sail's dependent type system, which is a light-weight system
balancing the benefits of static bounds and effects checking with the usability
of the language for engineers. I will also present the interface between the
instruction sets and concurrent models of the pipeline and memory systems,
whose requirements drove the development of our new language Sail.