NDLI: Inferable object-oriented typed assembly language

Please wait, while we are loading the content...

An analysis of the dynamic behavior of JavaScript programs

Safe programmable speculative parallelism

2010 Athena lecture

Safe to the last instruction: automated verification of a type-safe operating system

Schism: fragmentation-tolerant real-time garbage collection

Green: a framework for supporting energy-conscious programming using controlled approximation

Adversarial memory for detecting destructive races

Smooth interpretation

Line-up: a complete and automatic linearizability checker

FlumeJava: easy, efficient data-parallel pipelines

Mint: Java multi-stage programming using weak separability

Evaluating iterative optimization across 1000 datasets

Breadcrumbs: efficient context sensitivity for dynamic bug detection analyses

Supporting speculative parallelization in the presence of dynamic data structures

Bringing extensibility to verified compilers

Detecting inefficiently-used containers to avoid bloat

GUESSTIMATE: a programming model for collaborative distributed systems

PACER: proportional detection of data races

The reachability-bound problem

MemSAT: checking axiomatic specifications of memory models

Composing parallel software efficiently with lithe

Type-preserving compilation of end-to-end verification of security enforcement

Software data spreading: leveraging distributed caches to improve single thread performance

Decoupled lifeguards: enabling path optimizations for dynamic correctness checking tools

Cache topology aware computation mapping for multicores

Ur: statically-typed metaprogramming with type-level record computation

Finding low-utility data structures

A context-free markup language for semi-structured text

Lock elision for read-only critical sections in Java

Resolving and exploiting the k-CFA paradox: illuminating functional vs. object-oriented program analysis

DRFX: a simple and efficient memory model for concurrent programming languages

Bamboo: a data-centric, object-oriented approach to many-core software

Inferable object-oriented typed assembly language

Z-rays: divide arrays and conquer speed and flexibility

Jinn: synthesizing dynamic bug detectors for foreign language interfaces

A GPGPU compiler for memory optimization and parallelism management

Parameterized verification of transactional memories

Evaluating the accuracy of Java profilers

Printing floating-point numbers quickly and accurately with integers

Complete functional synthesis

Mixing type checking and symbolic execution

Traceable data types for self-adjusting computation

Inferable object-oriented typed assembly language

Content Provider	ACM Digital Library
Author	Hawblitzel, Chris Tate, Ross Chen, Juan
Abstract	A certifying compiler preserves type information through compilation to assembly language programs, producing typed assembly language (TAL) programs that can be verified for safety independently so that the compiler does not need to be trusted. There are two challenges for adopting certifying compilation in practice. First, requiring every compiler transformation and optimization to preserve types is a large burden on compilers, especially when adopting certifying compilation into existing optimizing non-certifying compilers. Second, type annotations significantly increase the size of assembly language programs. This paper proposes an alternative to traditional certifying compilers. It presents iTalX, the first inferable TAL type system that supports existential types, arrays, interfaces, and stacks. We have proved our inference algorithm is complete, meaning if an assembly language program is typeable with iTalX then our algorithm will infer an iTalX typing for that program. Furthermore, our algorithm is guaranteed to terminate even if the assembly language program is untypeable. We demonstrate that it is practical to infer such an expressive TAL by showing a prototype implementation of type inference for code compiled by Bartok, an optimizing C# compiler. Our prototype implementation infers complete type annotations for 98% of functions in a suite of realistic C# benchmarks. The type-inference time is about 8% of the compilation time. We needed to change only 2.5% of the compiler code, mostly adding new code for defining types and for writing types to object files. Most transformations are untouched. Type-annotation size is only 17% of the size of pure code and data, reducing type annotations in our previous certifying compiler [4] by 60%. The compiler needs to preserve only essential type information such as method signatures, object-layout information, and types for static data and external labels. Even non-certifying compilers have most of this information available.
Starting Page	424
Ending Page	435
Page Count	12
File Format	PDF
ISBN	9781450300193
DOI	10.1145/1806596.1806644
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2010-06-05
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Type inference Typed assembly language (tal) Certifying compiler Existential quantification Object-oriented compiler
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in