PhD course - Coccinelle: A Program Matching and Transformation Tool for Systems Code
Lectures:
Julia Lawall, INRIA
Date(s) of the course:
March 6-7, 2014
Time:
March 6, 2014: 13:30-17:00
March 7, 2014: 09:00-12:00
Place:
The course takes place at the IT University of Copenhagen, Rued Langgaardsvej 7, DK-2300 Copenhagen S, Denmark (www.itu.dk), in room 4A05
Course description:
Coccinelle is a program matching and transformation tool for C code, founded on the notion of a semantic patch, in which matching and transformation specifications are expressed using a patch-like syntax. Coccinelle has been extensively used for bug finding and evolution in the context of the Linux kernel, and other C software. This course will provide an overview of Coccinelle and its use on Linux code, as well as describing its internal design, based on a novel variant of the temporal logic CTL.
The course will introduce a number of Coccinelle features, including the use of metavariables, the use of isomorphisms, the matching of control-flow paths, the use of iteration, and the scripting language interface. Several real-sized examples will be considered in detail, addressing both bug finding and automating evolutions in the Linux kernel. Numerous exercises will be provided to be worked during the class period. Students wishing to use their own laptops should install Coccinelle as well as downloading the source code of Linux 3.2 (www.kernel.org).
Reading list: Required readin
- Dawson R. Engler, Benjamin Chelf, Andy Chou, Seth Hallem: Checking System Rules Using System-Specific, Programmer-Written Compiler Extensions. OSDI 2000: 1-16
- Yoann Padioleau, Julia L. Lawall, Gilles Muller: Understanding collateral evolution in Linux device drivers. EuroSys 2006: 59-71
- Yoann Padioleau, Julia L. Lawall, René Rydhof Hansen, Gilles Muller: Documenting and automating collateral evolutions in linux device drivers. EuroSys 2008: 247-260
Optional reading:
- Zhenmin Li, Shan Lu, Suvda Myagmar, Yuanyuan Zhou: CP-Miner: A Tool for Finding Copy-paste and Related Bugs in Operating System Code. OSDI 2004: 289-302
- Zhenmin Li, Yuanyuan Zhou: PR-Miner: automatically extracting implicit programming rules and detecting violations in large software code. ESEC/SIGSOFT FSE 2005: 306-315
- Nicolas Palix, Gaël Thomas, Suman Saha, Christophe Calvès, Julia L. Lawall, Gilles Muller: Faults in Linux: ten years later. ASPLOS 2011: 305-318
- Asim Kadav, Michael M. Swift: Understanding modern device drivers. ASPLOS 2012: 87-98
- Suman Saha, Jean-Pierre Lozi, Gaël Thomas, Julia L. Lawall, Gilles Muller: Hector: Detecting Resource-Release Omission Faults in error-handling code for systems software. DSN 2013: 1-12
Credits: 1 ECTS
How to sign up:
Sign up by sending an e-mail to Aleksandar Dimovski (adim@itu.dk).
Website:
Can be found here