5 ms·

F# RISC-V Instruction Set Formal Specification

122 points by adamnemecek 7y ago

deleted 7y ago
[deleted]
tom_mellior 7y ago
To me "formal specification" sounds like it should have some sort of connection to formal methods, i.e., some proof system. This looks more like what I would call an "instruction set simulator". Though if the focus is on clarity and readability rather than performance, "executable specification" might be a good middle ground.
- contravariant 7y ago
  In this context "formal" just means that no parts are left open to interpretation [1]. While proof systems are definitely formal that implication doesn't work the other way around. Under normal circumstances programming code is unambiguous and should therefore suffice as a formal definition / specification (with most programming errors stemming from the fact that this formal definition doesn't match the informal definition the programmer or customer had in mind). [1]: For comparison, https://en.wiktionary.org/wiki/formal https://en.wiktionary.org/wiki/formal defines 'formal' as: "(mathematics) Relating to mere manipulation and construction of strings of symbols, without regard to their meaning".
  - deleted 7y ago
    [deleted]
  - tom_mellior 7y ago
    > In this context "formal" just means that no parts are left open to interpretation Yes. But as you say, by that token any instruction set simulator could be called a "formal specification" (modulo undefined behavior, or if you deliberately wrote in a language with nondeterminism). But we don't call them that, because (I maintain) there is something more to being a "formal specification". Namely, being in a form that is easily amenable to formal methods tools, and the intention to apply these tools. Now of course a pure F# or Haskell program is much closer than C to being analyzed by formal methods tools, but there is still a gap that wouldn't be there if the specification were written directly in Coq or Agda or Isabelle or whatever.
    - contravariant 7y ago
      The main reason code isn't considered a formal specification is that it's not intended to be either formal or a specification. That doesn't mean you cannot write a formal specification in code. If anything code allows for a higher level of formality than all but the most formal mathematics. Which is why some mathematicians are advocating that mathematical proofs should be specified as code [1]. You shouldn't confuse the existence of these languages to mean that any code not capable of expressing mathematical proofs is not formal. It might be limited, but not informal. [1]: https://www.youtube.com/watch?v=Dp-mQ3HxgDE https://www.youtube.com/watch?v=Dp-mQ3HxgDE
- monocasa 7y ago
  It's the first step in a lot of formal methods. Like proving an implementation's adherence to the model requires a machine readable model. Or proving certain aspects about the model. For instance part of sel4's proof chain is a machine readable model of an ARM. It then uses that to prove equivalence of the generated binary to the high level spec of the kernel.
zmix 7y ago
Coming from a different background, I wonder what this project tries to achieve? And why F#?
- adamnemecek 7y ago
  What other language? Haskal is too much, Python is too little, Rust is essentially F#.
  - zingplex 7y ago
    Could you elaborate on why something like Haskell is too much? Similarly, why is Python too little?
    - adamnemecek 7y ago
      Python gives you too little in terms of formal verification. Haskell is hard to map to other langs.
- UK-Al05 7y ago
  Why not f#? I would imagine it has good support for discrimated unions which are quite good for representing instruction sets. He wanted a more modern platform than ocaml, or ml. He didn't want to go too deep down into the functional rabbit hole(haskell), and he didn't want to think about memory management at all(rust).
- Svoka 7y ago
  I find it strange that this comment is downvoted, while being only comment here asking "what does it do". As far as I understand this can be used as emulator of RISC-V processor. It is also has very verbose and clear code, so one can learn RISC-V instruction set reading it. It is specification written in programming language, which is a good reference. I find it easier to read than documentation, for example. F# is because it's as good programming language as any.
  - zmix 7y ago
justincormack 7y ago
There are multiple WIP formal specs for Risc-V it seems one will be chosen as official and is then likely to be used for further tooling eg hardware and software verification.
sanxiyn 7y ago
Here is one in Haskell which is more complete: https://github.com/mit-plv/riscv-semantics https://github.com/mit-plv/riscv-semantics. For example, it supports 64-bit ISA while this one doesn't yet.
szemet 7y ago
Maybe it could be ported to SML, because: > "It is distinctive among widely used languages in that it has a formal specification, given as typing rules and operational semantics in The Definition of Standard ML (1990, revised and simplified as The Definition of Standard ML (Revised) in 1997)." https://en.wikipedia.org/wiki/Standard_ML https://en.wikipedia.org/wiki/Standard_ML edit, the specification itself: http://sml-family.org/sml97-defn.pdf http://sml-family.org/sml97-defn.pdf
joshsyn 7y ago
Would make up a great blog post, about highlighting the weaknesses and strength of F#, if there are any?

122 points by adamnemecek 7y ago

deleted 7y ago

[deleted]

To me "formal specification" sounds like it should have some sort of connection to formal methods, i.e., some proof system. This looks more like what I would call an "instruction set simulator". Though if the focus is on clarity and readability rather than performance, "executable specification" might be a good middle ground.

contravariant 7y ago
In this context "formal" just means that no parts are left open to interpretation [1]. While proof systems are definitely formal that implication doesn't work the other way around. Under normal circumstances programming code is unambiguous and should therefore suffice as a formal definition / specification (with most programming errors stemming from the fact that this formal definition doesn't match the informal definition the programmer or customer had in mind). [1]: For comparison, https://en.wiktionary.org/wiki/formal https://en.wiktionary.org/wiki/formal defines 'formal' as: "(mathematics) Relating to mere manipulation and construction of strings of symbols, without regard to their meaning".
- deleted 7y ago
  [deleted]
- tom_mellior 7y ago
  > In this context "formal" just means that no parts are left open to interpretation Yes. But as you say, by that token any instruction set simulator could be called a "formal specification" (modulo undefined behavior, or if you deliberately wrote in a language with nondeterminism). But we don't call them that, because (I maintain) there is something more to being a "formal specification". Namely, being in a form that is easily amenable to formal methods tools, and the intention to apply these tools. Now of course a pure F# or Haskell program is much closer than C to being analyzed by formal methods tools, but there is still a gap that wouldn't be there if the specification were written directly in Coq or Agda or Isabelle or whatever.
  - contravariant 7y ago
    The main reason code isn't considered a formal specification is that it's not intended to be either formal or a specification. That doesn't mean you cannot write a formal specification in code. If anything code allows for a higher level of formality than all but the most formal mathematics. Which is why some mathematicians are advocating that mathematical proofs should be specified as code [1]. You shouldn't confuse the existence of these languages to mean that any code not capable of expressing mathematical proofs is not formal. It might be limited, but not informal. [1]: https://www.youtube.com/watch?v=Dp-mQ3HxgDE https://www.youtube.com/watch?v=Dp-mQ3HxgDE
monocasa 7y ago
It's the first step in a lot of formal methods. Like proving an implementation's adherence to the model requires a machine readable model. Or proving certain aspects about the model. For instance part of sel4's proof chain is a machine readable model of an ARM. It then uses that to prove equivalence of the generated binary to the high level spec of the kernel.

zmix 7y ago

Coming from a different background, I wonder what this project tries to achieve? And why F#?

adamnemecek 7y ago
What other language? Haskal is too much, Python is too little, Rust is essentially F#.
- zingplex 7y ago
  Could you elaborate on why something like Haskell is too much? Similarly, why is Python too little?
  - adamnemecek 7y ago
    Python gives you too little in terms of formal verification. Haskell is hard to map to other langs.
UK-Al05 7y ago
Why not f#? I would imagine it has good support for discrimated unions which are quite good for representing instruction sets. He wanted a more modern platform than ocaml, or ml. He didn't want to go too deep down into the functional rabbit hole(haskell), and he didn't want to think about memory management at all(rust).
Svoka 7y ago
I find it strange that this comment is downvoted, while being only comment here asking "what does it do". As far as I understand this can be used as emulator of RISC-V processor. It is also has very verbose and clear code, so one can learn RISC-V instruction set reading it. It is specification written in programming language, which is a good reference. I find it easier to read than documentation, for example. F# is because it's as good programming language as any.
- zmix 7y ago

justincormack 7y ago

There are multiple WIP formal specs for Risc-V it seems one will be chosen as official and is then likely to be used for further tooling eg hardware and software verification.

sanxiyn 7y ago

Here is one in Haskell which is more complete: https://github.com/mit-plv/riscv-semantics https://github.com/mit-plv/riscv-semantics. For example, it supports 64-bit ISA while this one doesn't yet.

szemet 7y ago

Maybe it could be ported to SML, because: > "It is distinctive among widely used languages in that it has a formal specification, given as typing rules and operational semantics in The Definition of Standard ML (1990, revised and simplified as The Definition of Standard ML (Revised) in 1997)." https://en.wikipedia.org/wiki/Standard_ML https://en.wikipedia.org/wiki/Standard_ML edit, the specification itself: http://sml-family.org/sml97-defn.pdf http://sml-family.org/sml97-defn.pdf

joshsyn 7y ago

Would make up a great blog post, about highlighting the weaknesses and strength of F#, if there are any?