The Sail ISA specification language | Hacker News Reader

The Sail ISA specification language

github.com

I wonder whether you could use Sail to make a compiler that figures out how to compile things. Then you could re-target it just by giving it a description of the new processor instead of a description of the old one.

Difficult problem!

If you don't care about compiler performance, auto-generating a compiler backend from scratch is already highly non-trivial. Sail's constrained nature may help a little but not that much, as you essentially need to auto-understand an interpreter for a Turing-complete language. If you do want performance, the problem becomes much harder still. One of the biggest problems in compiler performance is the memory model: what reordering is permitted, what is prohibited to the optimiser? Sail does not address this. Instead, (like all similar languages) it 'handles' main memory access by two uninterpreted functions which are (roughly) "memory read" and "memory write" That's a polite way of saying: Sail (like all similar languages) leaves this particular problem to the user.

There are open research questions here.

If you get the compiler backend generated then that same description language could also provide optimization hints. If you look at the RISC-V spec a lot is left up to the implementation but certain optimizations leave e.g. instructions available for cache management and this would have to be exposed in the ISA description.

Save Intel's compiler, do any rely on implementation details? They rely on cache and fetch details, but only in broad, nebulous ways that seem very portable.

There may be open research questions but it seems to me the biggest thing is paying someone to do it.

> highly non-trivial

I think you a word while reading.

There's work along these lines (substantially predating Sail, but one could in principle do much the same starting from Sail specs) by Dias and Ramsey, e.g. the POPL 2010 and 2011 papers at https://www.cs.tufts.edu/~nr/

This is how Go's assembler works.

When I worked at a large US-Based CPU company about 10 years ago I was always wondering why we didn't have a tool like this. Instead the ISA semantics were described in multiple word docs. Everything was mostly* manually created from those docs - it was fraught with the possibility of error. I did hear from someone who had worked at the same company in the 90s that they had had a tool akin to Sail back then that was based on an ML language (Oh, and it seems Sail is written in OCaml!) - it seems like Nirvana had been achieved then, but then paradise was lost by the time I was working there.

*'mostly' because there was a research group that was working on tools that would read the word docs and do some automation, though they seemed mostly still experimental... and it also seemed like a really bad way to approach the problem, but they were working with what the designers were used to - Word Docs.

Curiously, not the first with this name in the hardware description space. SAIL (all caps), the Stanford AI Language, was an Algol flavored beast from the 70s. VLSI Technology (eaten by Philips) used it for internal CAD tools like place and route, layout, etc. in the 90s. They liked it so much they had an internal tools group maintaining it, along with very heavy use of ClearCase.

https://en.wikipedia.org/wiki/SAIL_(programming_language)

https://en.wikipedia.org/wiki/VLSI_Technology

I thought I'd heard of this before. In fact when I saw "Sail" here in the title I figured it was the one you were referring to.

Can it model an ISA like the Mill?

I don't know, but that's not the goal. REMS stands for Rigorous Engineering of Mainstream Systems. Mill is not a mainstream system.

Yeah, at it's core, Sail is an RTL. It shouldn't have a problem with the Mill, but it probably isn't the most ergonomic arch for Sail.

Sail is not at the register-transfer level (RTL) [1].

Why? Because Sail does not offer abstractions for clocked digital circuits, which is what characterises the RTL. The most widely used DSL for the RTL is (System)Verilog [3]. Instead, Sail is a stand-alone DSL for the ISA (= instruction set architecture). The purpose of the ISA level is to talk about that a processor looks from the outside, to the programmer (most specifically to the compiler writer). Sail is a minimal programming language with a single purpose: writing ISA specifications, which means writing an interpreter for assembly language. Technically, Sail is a simple imperative language with first-order functions. What makes Sail suitable for specifying ISAs is its typing system. Sail supports types that are frequently used in ISA interpreters, such as dependent typing for numeric types and bitvector lengths. Sail is closely related to Arm's ASL (= architecture specification language) [2].

Since Sail is Turing-complete, any ISA can be modelled, including Mill. For the same reason any RTL can be modelled, for example by coding up an interpreter for an RTL language like Verilog, but that would be mighty inconvenient.

[1] https://en.wikipedia.org/wiki/Register-transfer_level

[2] https://alastairreid.github.io/ARM-v8a-xml-release/

[3] https://en.wikipedia.org/wiki/Verilog

There are RTLs that aren't HDLs.

For instance one of GCCs intermediate representations really reminds me of Sail. https://gcc.gnu.org/onlinedocs/gccint/RTL.html

I see now where the confusion comes from: the abbreviation RTL is overloaded to (1) register-transfer level (as e.g. Verilog) and (2) register-transfer language (e.g. GCCs intermediate representation you cited). I think the former use is much more widespread. I agree GCC's register-transfer language is close to Sail.

Reply on news.ycombinator.com