1. 11
  1.  

  2. 4

    Main paper:

    https://www.cs.cornell.edu/talc/papers/talx86-wcsss.pdf

    This group did a lot of great work in late 90’s and early to mid 2000’s knocking out many aspects of safety for low-level programming. That included things like linear types. One highlight from the group is that Greg Morrisett wrote Cyclone language, a safer C, using stuff he learned there. It’s safety model was an inspiration for Rust’s. There could be other things that trace back to these projects.

    1. 6

      There seems to be no research on typed assembly after 2000? I recognize names like Stephanie Weirich, Trevor Jim, Steve Zdancewic, who all continued to work on higher levels (Cyclone, Haskell, etc). A bytecode/assembly specialized on safety and sandboxing is not available today. The idea to use an expressive type system feels nice.

      I do not fully buy their criticism of JVML in the paper you linked.

      1. They criticize the non-formal post-hoc description of JVML? They build TALx86 post-hoc for the x86 ISA.

      2. This I agree to. I usually criticize the lack of structs in JVML.

      3. They criticize that Java must be JITed to be fast. Their x86 subset would have to be JITed to be fast today as well. Under Future Work they claim that adding support for floating point and MMX would not be difficult. Today with ever more ISA extension that would be harder.

      Is there a fundamental difference between bytecode and assembly? You could define one as stack-based and the later register-based, but that seems shallow to me.

      1. 4

        “They criticize the non-formal post-hoc description of JVML? They build TALx86 post-hoc for the x86 ISA.” “Their x86 subset would have to be JITed to be fast today as well. “

        Haha. Nice.

        “ they claim that adding support for floating point and MMX would not be difficult.”

        Idk about MMX but Leroy et al are laying down lots of groundwork for future efforts at floating point over at INRIA. They’ve been specifying and verifying it as part of their work on verified compilers. Next effort for floating point in TAL’s might prove the type system, checks or whatever using their stuff.

        There seems to be no research on typed assembly after 2000?

        Vast majority of work went into essentially modeling it in prover formalisms either to use in formally-verified compilers or equivalence checks (eg translation validation) on specs generated from assembly. The most, effective projects also started building on each other in these areas. That made it more sensible for people doing verification to default on putting their next work on it. This didn’t stop all TAL-style research, though. Here’s a few off top of head:

        https://www.cs.rice.edu/~taha/teaching/04H/RAP/cache/ltal-tr.pdf

        http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.419.4545&rep=rep1&type=pdf

        http://research.microsoft.com/en-us/um/people/nick/coqasm.pdf

        Note: Microsoft also did something at assembly level as part of VCC and Hyper-V efforts but my memory loss is blocking it right now. It was also harder to find papers on than VCC. I assume it’s either really, really good or too alpha for them to publish.

        I also found a few others with a quick Google that tie in:

        https://dl.acm.org/citation.cfm?id=2182144

        https://www.cs.princeton.edu/~dpw/papers/tal_ft-tr.pdf

        https://www.usenix.org/legacy/event/ssv10/tech/full_papers/Maeda.pdf

        Have fun! :)

        1. 4

          http://research.microsoft.com/en-us/um/people/nick/coqasm.pdf

          Want to highlight this one. “Coq: The world’s best macro assembler?” is a really great paper.

          1. 2

            I wished they FOSS’d it. I couldn’t find it when I looked for code to go with the paper back when it was published. Maybe they’ve done it by now. It was among MS Research’s greatest work given the implications for safe, performance-critical or just low-level code that could come out of it or expansions on it.

        2. 2

          Is there a fundamental difference between bytecode and assembly? You could define one as stack-based and the latter [as] register-based, but that seems shallow to me.

          Wikipedia shows examples of non-stack-based bytecode. I think “bytecode” is now just another name for “VM”, to contrast it with “real” machines like x86.

          I was thinking about this distinction as well because I’ve been mulling compiling Mu to a VM that just happens to be a subset of the x86 ISA.