Jinn: Synthesizing dynamic bug detectors for foreign language interfaces

Byeongcheol Lee, Ben Wiedermann, Martin Hirzel, Robert Grimm, Kathryn S. McKinley

Research output: Contribution to journalArticle

Abstract

Programming language specifications mandate static and dynamic analyses to preclude syntactic and semantic errors. Although individual languages are usually well-specified, composing languages is not, and this poor specification is a source of many errors in multilingual programs. For example, virtually all Java programs compose Java and C using the Java Native Interface (JNI). Since JNI is informally specified, developers have difficulty using it correctly, and current Java compilers and virtual machines (VMs) inconsistently check only a subset of JNI constraints. This paper's most significant contribution is to show how to synthesize dynamic analyses from state machines to detect foreign function interface (FFI) violations.We identify three classes of FFI constraints encoded by eleven state machines that capture thousands of JNI and Python/C FFI rules. We use a mapping function to specify which state machines, transitions, and program entities (threads, objects, references) to check at each FFI call and return. From this function, we synthesize a context-specific dynamic analysis to find FFI bugs. We build bug detection tools for JNI and Python/C using this approach. For JNI, we dynamically and transparently interpose the analysis on Java and C language transitions through the JVM tools interface. The resulting tool, called Jinn, is compiler and virtual machine independent. It detects and diagnoses a wide variety of FFI bugs that other tools miss. This approach greatly reduces the annotation burden by exploiting common FFI constraints: whereas the generated Jinn code is 22,000+ lines, we wrote only 1,400 lines of state machine and mapping code. Overall, this paper lays the foundation for a more principled approach to developing correct multilingual software and a more concise and automated approach to FFI specification.

Original languageEnglish (US)
Pages (from-to)36-49
Number of pages14
JournalACM SIGPLAN Notices
Volume45
Issue number6
DOIs
StatePublished - Jun 2010

Fingerprint

Detectors
Specifications
Syntactics
Computer programming languages
Dynamic analysis
Semantics

Keywords

  • Dynamic Analysis
  • FFI Bugs
  • Foreign Function Interfaces (FFI)
  • Java Native Interface (JNI)
  • Multilingual Programs
  • Python/C
  • Specification
  • Specification Generation

ASJC Scopus subject areas

  • Computer Science(all)

Cite this

Lee, B., Wiedermann, B., Hirzel, M., Grimm, R., & McKinley, K. S. (2010). Jinn: Synthesizing dynamic bug detectors for foreign language interfaces. ACM SIGPLAN Notices, 45(6), 36-49. https://doi.org/10.1145/1809028.1806601

Jinn : Synthesizing dynamic bug detectors for foreign language interfaces. / Lee, Byeongcheol; Wiedermann, Ben; Hirzel, Martin; Grimm, Robert; McKinley, Kathryn S.

In: ACM SIGPLAN Notices, Vol. 45, No. 6, 06.2010, p. 36-49.

Research output: Contribution to journalArticle

Lee, B, Wiedermann, B, Hirzel, M, Grimm, R & McKinley, KS 2010, 'Jinn: Synthesizing dynamic bug detectors for foreign language interfaces', ACM SIGPLAN Notices, vol. 45, no. 6, pp. 36-49. https://doi.org/10.1145/1809028.1806601
Lee, Byeongcheol ; Wiedermann, Ben ; Hirzel, Martin ; Grimm, Robert ; McKinley, Kathryn S. / Jinn : Synthesizing dynamic bug detectors for foreign language interfaces. In: ACM SIGPLAN Notices. 2010 ; Vol. 45, No. 6. pp. 36-49.
@article{7bdf250fd25b481ea889984e6741387a,
title = "Jinn: Synthesizing dynamic bug detectors for foreign language interfaces",
abstract = "Programming language specifications mandate static and dynamic analyses to preclude syntactic and semantic errors. Although individual languages are usually well-specified, composing languages is not, and this poor specification is a source of many errors in multilingual programs. For example, virtually all Java programs compose Java and C using the Java Native Interface (JNI). Since JNI is informally specified, developers have difficulty using it correctly, and current Java compilers and virtual machines (VMs) inconsistently check only a subset of JNI constraints. This paper's most significant contribution is to show how to synthesize dynamic analyses from state machines to detect foreign function interface (FFI) violations.We identify three classes of FFI constraints encoded by eleven state machines that capture thousands of JNI and Python/C FFI rules. We use a mapping function to specify which state machines, transitions, and program entities (threads, objects, references) to check at each FFI call and return. From this function, we synthesize a context-specific dynamic analysis to find FFI bugs. We build bug detection tools for JNI and Python/C using this approach. For JNI, we dynamically and transparently interpose the analysis on Java and C language transitions through the JVM tools interface. The resulting tool, called Jinn, is compiler and virtual machine independent. It detects and diagnoses a wide variety of FFI bugs that other tools miss. This approach greatly reduces the annotation burden by exploiting common FFI constraints: whereas the generated Jinn code is 22,000+ lines, we wrote only 1,400 lines of state machine and mapping code. Overall, this paper lays the foundation for a more principled approach to developing correct multilingual software and a more concise and automated approach to FFI specification.",
keywords = "Dynamic Analysis, FFI Bugs, Foreign Function Interfaces (FFI), Java Native Interface (JNI), Multilingual Programs, Python/C, Specification, Specification Generation",
author = "Byeongcheol Lee and Ben Wiedermann and Martin Hirzel and Robert Grimm and McKinley, {Kathryn S.}",
year = "2010",
month = "6",
doi = "10.1145/1809028.1806601",
language = "English (US)",
volume = "45",
pages = "36--49",
journal = "ACM SIGPLAN Notices",
issn = "1523-2867",
publisher = "Association for Computing Machinery (ACM)",
number = "6",

}

TY - JOUR

T1 - Jinn

T2 - Synthesizing dynamic bug detectors for foreign language interfaces

AU - Lee, Byeongcheol

AU - Wiedermann, Ben

AU - Hirzel, Martin

AU - Grimm, Robert

AU - McKinley, Kathryn S.

PY - 2010/6

Y1 - 2010/6

N2 - Programming language specifications mandate static and dynamic analyses to preclude syntactic and semantic errors. Although individual languages are usually well-specified, composing languages is not, and this poor specification is a source of many errors in multilingual programs. For example, virtually all Java programs compose Java and C using the Java Native Interface (JNI). Since JNI is informally specified, developers have difficulty using it correctly, and current Java compilers and virtual machines (VMs) inconsistently check only a subset of JNI constraints. This paper's most significant contribution is to show how to synthesize dynamic analyses from state machines to detect foreign function interface (FFI) violations.We identify three classes of FFI constraints encoded by eleven state machines that capture thousands of JNI and Python/C FFI rules. We use a mapping function to specify which state machines, transitions, and program entities (threads, objects, references) to check at each FFI call and return. From this function, we synthesize a context-specific dynamic analysis to find FFI bugs. We build bug detection tools for JNI and Python/C using this approach. For JNI, we dynamically and transparently interpose the analysis on Java and C language transitions through the JVM tools interface. The resulting tool, called Jinn, is compiler and virtual machine independent. It detects and diagnoses a wide variety of FFI bugs that other tools miss. This approach greatly reduces the annotation burden by exploiting common FFI constraints: whereas the generated Jinn code is 22,000+ lines, we wrote only 1,400 lines of state machine and mapping code. Overall, this paper lays the foundation for a more principled approach to developing correct multilingual software and a more concise and automated approach to FFI specification.

AB - Programming language specifications mandate static and dynamic analyses to preclude syntactic and semantic errors. Although individual languages are usually well-specified, composing languages is not, and this poor specification is a source of many errors in multilingual programs. For example, virtually all Java programs compose Java and C using the Java Native Interface (JNI). Since JNI is informally specified, developers have difficulty using it correctly, and current Java compilers and virtual machines (VMs) inconsistently check only a subset of JNI constraints. This paper's most significant contribution is to show how to synthesize dynamic analyses from state machines to detect foreign function interface (FFI) violations.We identify three classes of FFI constraints encoded by eleven state machines that capture thousands of JNI and Python/C FFI rules. We use a mapping function to specify which state machines, transitions, and program entities (threads, objects, references) to check at each FFI call and return. From this function, we synthesize a context-specific dynamic analysis to find FFI bugs. We build bug detection tools for JNI and Python/C using this approach. For JNI, we dynamically and transparently interpose the analysis on Java and C language transitions through the JVM tools interface. The resulting tool, called Jinn, is compiler and virtual machine independent. It detects and diagnoses a wide variety of FFI bugs that other tools miss. This approach greatly reduces the annotation burden by exploiting common FFI constraints: whereas the generated Jinn code is 22,000+ lines, we wrote only 1,400 lines of state machine and mapping code. Overall, this paper lays the foundation for a more principled approach to developing correct multilingual software and a more concise and automated approach to FFI specification.

KW - Dynamic Analysis

KW - FFI Bugs

KW - Foreign Function Interfaces (FFI)

KW - Java Native Interface (JNI)

KW - Multilingual Programs

KW - Python/C

KW - Specification

KW - Specification Generation

UR - http://www.scopus.com/inward/record.url?scp=77957574174&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=77957574174&partnerID=8YFLogxK

U2 - 10.1145/1809028.1806601

DO - 10.1145/1809028.1806601

M3 - Article

AN - SCOPUS:77957574174

VL - 45

SP - 36

EP - 49

JO - ACM SIGPLAN Notices

JF - ACM SIGPLAN Notices

SN - 1523-2867

IS - 6

ER -