Cyclone(ID:3312/cyc002)

Cornell and ATT Bell labs  

A Safe Dialect of C

Places
Related languages
C => Cyclone   Evolution of
Popcorn => Cyclone   Influence
TAL/T => Cyclone   Compiled to
References:
  • Hornof, Luke and Trevor Jim. Certifying Compilation and Run-time Code Generation view details Abstract: A certifying compiler takes a source language program and produces object code, as well as a "certificate'' that can be used to verify that the object code satisfies desirable properties, such as type safety and memory safety. Certifying compilation helps to increase both compiler robustness and program safety. Compiler robustness is improved since some compiler errors can be caught by checking the object code against the certificate immediately after compilation. Program safety is improved because the object code and certificate alone are sufficient to establish safety: even if the object code and certificate are produced on an unknown machine by an unknown compiler and sent over an untrusted network, safe execution is guaranteed as long as the code and certificate pass the verifier.

    Existing work in certifying compilation has addressed statically generated code. In this paper, we extend this to code generated at run time. Our goal is to combine certifying compilation with run-time code generation to produce programs that are both verifiably safe and extremely fast. To achieve this goal, we present two new languages with explicit run-time code generation constructs: Cyclone, a type safe dialect of C, and TAL/T, a type safe assembly language. We have designed and implemented a system that translates a safe C program into Cyclone, which is then compiled to TAL/T, and finally assembled into executable object code. This paper focuses on our overall approach and the front end of our system; details about TAL/T will appear in a subsequent paper.

    pdf
          in the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, San Antonio, TX, USA, January 1999. view details
  • Dan Grossman et al "Region-based Memory Management in Cyclone" view details pdf
          in ACM Conference on Programming Language Design and Implementation, Berlin, Germany, June, 2002 view details
  • Trevor Jim, Greg Morrisett, Dan Grossman, Michael Hicks, James Cheney, and Yanling Wang. "Cyclone: A Safe Dialect of C" view details pdf
          in USENIX Annual Technical Conference, Monterey, CA, June 2002 view details
    Resources
    • Cyclone home page
      http://www.cs.cornell.edu/projects/cyclone/external link
    • implementationand source at Cornell

      "
    • manual at Cornell

      "