TAL(ID:3708/tal002)

Assembly language for TALC 

for Typed Assembly Language

Stack-Based Typed Assembly Language

TALC project at Cornell, Greg Morrisett et al, 1997



Structures:
Related languages
TIL => TAL   Influence
TAL => Popcorn   Compiled to
TAL => TAL/T   Derivation of
References:
  • Frederick Smith and Greg Morrisett. Mostly-Copying Collection: A Viable Alternative to Conversative Mark-Sweep. Technical Report TR97-1644, Cornell University, August 1997. view details Abstract: Many high-level language compilers generate C code and then invoke a C compiler to do code generation, register allocation, stack management, and low-level optimization. To date, most of these compilers link the resulting code against a conservative mark-sweep garbage collector in order to reclaim unused memory. We introduce a new collector, MCC, based on mostly-copying collection, and characterize the conditions that favor such a collector over a mark-sweep collector.  In particular we demonstrate that mostly-copying collection outperforms conservative mark-sweep under the same conditions that accurate copying collection outperforms accurate mark-sweep: Specifically, MCC meets or exceeds the performance of a mature mark-sweep collector when allocation rates are high, and physical memory is large relative to the live
    data. pdf
  • Morrisett, Greg; David Walker, Karl Crary, and Neal Glew. From System F to Typed Assembly Language (Extended version). Technical Report TR97-1651, Cornell University, November 1997. view details Abstract: We motivate the design of a statically typed assembly language (TAL) and present a type-preserving translation from System F to TAL. The TAL we present is based on a conventional RISC assembly language, but its static type system provides support for enforcing high-level language abstractions, such as closures, tuples, and objects, as well as user-defined abstract data types. The type system ensures that well-typed programs cannot violate these abstractions. In addition, the typing constructs place almost no restrictions on low-level optimizations such as register allocation, instruction selection, or instruction scheduling.

    Our translation to TAL is specified as a sequence of type-preserving transformations, including CPS and closure conversion phases; type-correct source programs are mapped to type-correct assembly language. A key contribution is an approach to polymorphic closure conversion that is considerably simpler than previous work. The compiler and typed assembly language provide a fully automatic way to produce proof carrying code, suitable for use in systems where untrusted and potentially malicious code must be checked for safety before execution. pdf
  • Crary, Karl ; Stephanie Weirich, and Greg Morrisett. Intensional Polymorphism in Type-Erasure Semantics (Extended version). Technical Report TR98-1721, Cornell University, November 1998. view details
  • Crary, Karl ; Stephanie Weirich, and Greg Morrisett. Intensional Polymorphism in Type-Erasure Semantics. 1998 International Conference on Functional Programming, pages 301-312, Baltimore, September 1998. view details
  • Morrisett, Greg; David Walker, Karl Crary, and Neal Glew. From System F to Typed Assembly Language. view details
          in The Twenty-Fifth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, CA, USA, January 1998 view details
  • Morrisett, Greg; Karl Crary, Neal Glew, and David Walker. Stack-Based Typed Assembly Language (Extended version). Technical Report CMU-CS-98-178, Carnegie Mellon University, December 1998. view details
          in The Twenty-Fifth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, CA, USA, January 1998 view details
  • Morrisett, Greg; Karl Crary, Neal Glew, and David Walker. Stack-Based Typed Assembly Language. In the 1998 Workshop on Types in Compilation, Kyoto, Japan, March 1998. Published in Xavier Leroy and Atsushi Ohori, editors, Lecture Notes in Computer Science, volume 1473, pages 28-52. Springer-Verlag, 1998. view details
          in The Twenty-Fifth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, CA, USA, January 1998 view details
  • Smith, Frederick and Greg Morrisett "Comparing Mostly-Copying and Mark-Sweep Conversative Collection" pp68-78 view details Abstract: Many high-level language compilers generate C code and then invoke a C compiler for code generation, register allocation, stack management, and low-level optimization. To date, most of these compilers link the resulting code against a conservative mark-sweep garbage collector in order to reclaim unused memory. We introduce a new collector, MCC, based on an extension of mostly-copying collection.

    We analyze the various design decisions made in MCC and provide a performance comparison to the most widely used conservative mark-sweep collector (the Boehm-Demers-Weiser collector). Our results show that a good mostly-copying collector can outperform a mature highly-optimized mark-sweep collector when physical memory is large relative to the live data. A surprising result of our analysis is that cache behavior has a greater impact on overall performance than either collector time, or allocation code. pdf
          in 1998 International Symposium on Memory Management, Vancouver, Canada, October 1998 view details
  • Crary, Karl "A Simple Proof Technique for Certain Parametricity Results" view details
          in In the 1999 ACM SIGPLAN International Conference on Functional Programming, Paris, France, September 1999. view details
  • Crary, Karl ; David Walker, and Greg Morrisett. Typed Memory Management in a Calculus of Capabilities view details Abstract: An increasing number of systems rely on programming language technology to ensure safety and security of low-level code. Unfortunately, these systems typically rely on a complex, trusted garbage collector. Region-based type systems provide an alternative to garbage collection by making memory management explicit but verifiably safe. However, it has not been clear how to use regions in low-level, type-safe code.

    We present a compiler intermediate language, called the Capability Calculus, that supports region-based memory management, enjoys a provably safe type system, and is straightforward to compile to a typed assembly language. Source languages may be compiled to our language using known region inference algorithms. Furthermore, region lifetimes need not be lexically scoped in our language, yet the language may be checked for safety without complex analyses. Finally, our soundness proof is relatively simple, employing only standard techniques.

    The central novelty is the use of static capabilities to specify the permissibility of various operations, such as memory access and deallocation. In order to ensure capabilities are relinquished properly, the type system tracks aliasing information using a form of bounded quantification.
    pdf
          in [ACM SIGACT-SIGPLAN] The Twenty-Sixth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, USA, January 1999. view details
  • Crary, Karl and Weirich, Stephanie "Flexible Type Analysis" view details
          in In the 1999 ACM SIGPLAN International Conference on Functional Programming, Paris, France, September 1999. view details
  • Frederick Smith, David Walker and Greg Morrisett. Alias Types. Technical Report TR99-1773, Cornell University, October 1999. view details
          in In the 1999 ACM SIGPLAN International Conference on Functional Programming, Paris, France, September 1999. view details
  • Glew, Neal "Type Dispatch for Named Hierarchical Types" view details
          in In the 1999 ACM SIGPLAN International Conference on Functional Programming, Paris, France, September 1999. view details
  • Glew, Neal and Greg Morrisett. Type-Safe Linking and Modular Assembly Language. view details
          in [ACM SIGACT-SIGPLAN] The Twenty-Sixth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, USA, January 1999. view details
  • Glew, Neal Object Closure Conversion. In the 3rd International Workshop on Higher Order Operational Techniques in Semantics, Paris, France, September 1999. view details
          in [ACM SIGACT-SIGPLAN] The Twenty-Sixth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, USA, January 1999. view details
  • Glew, Neal Object Closure Conversion. Technical Report TR99-1763, Cornell University, August 1999. view details
          in [ACM SIGACT-SIGPLAN] The Twenty-Sixth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, USA, January 1999. view details
  • Glew, Neal Type Dispatch for Named Hierarchical Types. Technical Report TR99-1738, Cornell University, April 1999. view details
          in [ACM SIGACT-SIGPLAN] The Twenty-Sixth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, USA, January 1999. view details
  • Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. "TALx86: A Realistic Typed Assembly Language" view details
          in Proceedings of the 1999 ACM SIGPLAN Workshop on Compiler Support for System Software, Atlanta, GA, USA, May 1999. view details
  • 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
  • Morrisett, Greg; David Walker, Karl Crary, and Neal Glew. From System F to Typed Assembly Language. In ACM Transactions on Programming Languages and Systems, 21(3):528-569, May 1999. view details
          in the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, San Antonio, TX, USA, January 1999. view details
  • Smith, Frederick; Walker, David and Greg Morrisett. "Alias Types" view details
          in European Symposium On Programming (ESOP'99), Lecture Notes in Computer Science view details
  • Walker. David A Type System for Expressive Security Policies. Technical Report TR99-1740, Cornell University, April 1999 view details
          in European Symposium On Programming (ESOP'99), Lecture Notes in Computer Science view details
  • Zdancewic, Steve and Dan Grossman. Principals in Programming Languages: Technical Results. Technical Report TR99-1752, Cornell University, June 1999. view details
          in European Symposium On Programming (ESOP'99), Lecture Notes in Computer Science view details
  • Zdancewic, Steve; Grossman, Dan and Greg Morrisett. "Principals in Programming Languages: A Syntactic Proof Technique" view details
          in In the 1999 ACM SIGPLAN International Conference on Functional Programming, Paris, France, September 1999. view details
  • Crary Karl and Stephanie Weirich. Resource Bound Certification view details
          in [ACM SIGACT-SIGPLAN] 27th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'00), Boston, Massachusetts, January 19-21, 2000 view details
  • Crary, Karl ; Michael Hicks and Stephanie Weirich. Safe and Flexible Dynamic Linking of Native Code view details
          in The 2000 ACM SIGPLAN Workshop on Types in Compilation, Montreal, Canada, September 2000. view details
  • Frederick Smith, Dan Grossman, Greg Morrisett, Luke Hornof, Trevor Jim. Compiling for Runtime Code Generation (Extended Version). Technical Report TR2000-1824, Cornell University, October 2000. view details
          in The 2000 ACM SIGPLAN Workshop on Types in Compilation, Montreal, Canada, September 2000. view details
  • Grossman, Dan and Greg Morrisett. Scalable Certification for Typed Assembly Language. view details
          in The 2000 ACM SIGPLAN Workshop on Types in Compilation, Montreal, Canada, September 2000. view details
  • Grossman, Dan and Greg Morrisett. Scalable Certification of Native Code: Experience from Compiling to TALx86. Technical Report TR2000-1783, Cornell University, February 2000. view details
          in The 2000 ACM SIGPLAN Workshop on Types in Compilation, Montreal, Canada, September 2000. view details
  • Walker, David A "Type System for Expressive Security Properties" view details
          in [ACM SIGACT-SIGPLAN] 27th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'00), Boston, Massachusetts, January 19-21, 2000 view details
  • Walker, David and Greg Morrisett. Alias Types for Recursive Data Structures. Technical Report TR2000-1787, Cornell University, March 2000. view details
          in [ACM SIGACT-SIGPLAN] 27th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'00), Boston, Massachusetts, January 19-21, 2000 view details
  • Walker, David Karl Crary and Greg Morrisett. Typed Memory Management in a Calculus of Capabilities. Technical Report TR2000-1780, Cornell University, February 2000. view details
          in [ACM SIGACT-SIGPLAN] 27th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'00), Boston, Massachusetts, January 19-21, 2000 view details