Write a Blog >>
Fri 24 Jan 2020 14:21 - 14:43 at Ile de France III (IDF III) - Language Design Chair(s): Amin Timany

The POSIX shell is a widely deployed, powerful tool for managing computer systems. The shell is the expert’s control panel, a necessary tool for configuring, compiling, installing, maintaining, and deploying systems. Even though it is powerful, critical infrastructure, the POSIX shell is maligned and misunderstood. Its power and its subtlety are a dangerous combination.

We define a formal, mechanized, executable small-step semantics for the POSIX shell, which we call Smoosh. We compared Smoosh against seven other shells that aim for some measure of POSIX compliance (bash, dash, zsh, OSH, mksh, ksh93, and yash). Using three test suites—the POSIX test suite, the Modernish test suite and shell diagnosis, and a test suite of our own device—we found Smoosh’s semantics to be the most conformant to the POSIX standard. Modernish judges Smoosh to have the fewest bugs (just one, from using dash’s parser) and no quirks. To show that our semantics is useful beyond yielding a conformant, executable shell, we also implemented a symbolic stepper to illuminate the subtle behavior of the shell.

Smoosh will serve as a foundation for formal study of the POSIX shell, supporting research on and development of new shells, new tooling for shells, and new shell designs.

Executable Formal Semantics for the POSIX Shell (smoosh.key)2.95MiB

Fri 24 Jan
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

14:00 - 15:05: Research Papers - Language Design at Ile de France III (IDF III)
Chair(s): Amin Timanyimec-Distrinet KU-Leuven
POPL-2020-Research-Papers14:00 - 14:21
Ralf JungMPI-SWS, Hoang-Hai DangMPI-SWS, Jeehoon KangKAIST, Derek DreyerMPI-SWS
Link to publication DOI Media Attached File Attached
POPL-2020-Research-Papers14:21 - 14:43
Michael GreenbergPomona College, Austin J. BlattPuppet Labs
Link to publication DOI Media Attached File Attached
POPL-2020-Research-Papers14:43 - 15:05
Sam WestrickCarnegie Mellon University, Rohan YadavCarnegie Mellon University, Matthew FluetRochester Institute of Technology, Umut A. AcarCarnegie Mellon University
Link to publication DOI Media Attached File Attached