skip to main content
10.1145/1287624.1287636acmconferencesArticle/Chapter ViewAbstractPublication PagesfseConference Proceedingsconference-collections
Article

Programming asynchronous layers with CLARITY

Published: 07 September 2007 Publication History

Abstract

Asynchronous systems components are hard to write, hard to reason about, and (not coincidentally) hard to mechanically verify. In order to achieve high performance, asynchronous code is often written in an event-driven style that introduces non-sequential control flow and persistent heap data to track pending operations. As a result, existing sequential verification and static analysis tools are ineffective on event-driven code.
We describe CLARITY, a programming language that enables analyzable design of asynchronous components. Clarity has three novel features: (1) Nonblocking function calls which allow event-driven code to be written in a sequential style. If a blocking statement is encountered during the execution of such a call, the call returns and the remainder of the operation is automatically queued for later execution. (2) Coords, a set of high-level coordination primitives, which encapsulate common interactions between asynchronous components and make high-level coordination protocols explicit. (3) Linearity annotations, which delegate coord protocol obligations to exactly one thread at each asynchronous function call, transforming a concurrent analysis problem into a sequential one.
We demonstrate how these language features enable both a more intuitive expression of program logic and more effective program analysis---most checking is done using simple sequential analysis. We describe our experience in developing a network device driver with CLARITY. We are able to mechanically verify several properties of the CLARITY driver that are beyond the reach of current analysis technology applied to equivalent C code.

References

[1]
A. Adya, J. Howell, M. Theimer, W. J. Bolosky, and J. R. Douceur. Cooperative task management without manual stack management. In Usenix Annual Tech. Conf., June 2002.
[2]
T. Andrews, S. Qadeer, S. K. Rajamani, J. Rehof, and Y. Xie. Zing: Exploiting program structure for model checking concurrent software. In CONCUR, volume 3170 of LNCS, 2004. Invited paper.
[3]
T. Arons, A. Pnueli, S. Ruah, Y. Xu, and L. D. Zuck. Parameterized verification with automatically computed inductive assertions. In CAV, volume 2102 of LNCS, pages 221--234, 2001.
[4]
T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In SPIN Workshop, volume 2057 of LNCS, 2001.
[5]
T. Ball and S. K. Rajamani. SLIC: A specification language for interface checking of C. Technical Report MSR-TR-2001-21, Microsoft Research, Jan. 2001.
[6]
G. Berry and G. Gonthier. The Esterel synchronous programming language: Design, semantics, implementation. Sci. Comput. Programming, 19(2):87--152, 1992.
[7]
R. D. Blumofe, C. F. Joerg, B. Kuszmaul, C. E. Leiserson, K. H. Randall, and Y. Zhou. Cilk: An efficient multithreaded runtime system. In PPoPP, pages 207--216, Santa Barbara, CA, July 1995.
[8]
P. Brinch Hansen. The programming language Concurrent Pascal. IEEE Trans. Softw. Eng., 1(2):199--207, 1975.
[9]
S. Chandra, B. Richards, and J. R. Larus. Teapot: A domain-specific language for writing cache coherence protocols. IEEE Trans. Softw. Eng., 25(3):317--333, 1999.
[10]
P. Chandrasekaran, C. L. Conway, J. M. Joy, and S. K. Rajamani. Programming asynchronous layers with CLARITY. Technical Report MSR-TR-2007-80, Microsoft Research, 2007.
[11]
M. Das, S. Lerner, and M. Seigle. ESP: Path-sensitive program verification in polynomial time. In PLDI, pages 57--69, 2002.
[12]
L. de Alfaro and T. A. Henzinger. Interface automata. In FSE, pages 109--120, 2001.
[13]
D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In OSDI, 2000.
[14]
Ú. Erlingsson and F. B. Schneider. SASI enforcement of security policies: A retrospective. Technical Report 1999--1758, Cornell University, Ithaca, NY, 1999.
[15]
M. Fähndrich and R. DeLine. Adoption and focus: Practical linear types for imperative programming. In PLDI, pages 13--24, 2002.
[16]
N. Halbwachs, F. Lagnier, and P. Raymond. Synchronous observers and the verification of reactive systems. In Algebraic Methodology and Software Technology, June 1993.
[17]
R. H. Halstead. MULTILISP: a language for concurrent symbolic computation. ACM Trans. Prog. Lang. Syst., 7(4):501--538, October 1985.
[18]
T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL, pages 58--70, 2002.
[19]
C. A. R. Hoare. Monitors: An operating system structuring concept. Commun. ACM, 17(10):549--557, Oct. 1974.
[20]
C. A. R. Hoare. Communicating sequential processes. Commun. ACM, 21(8):666--677, 1978.
[21]
ISO Standard - Programming Languages - C, Dec. 1999. ISO/IEC 9899:1999.
[22]
L. Lamport. A new solution of Dijkstra's concurrent programming problem. Commun. ACM, 17(8):453--455, Aug. 1974.
[23]
J. R. Larus and M. Parkes. Using cohort scheduling to enhance server performance. Technical Report MSR-TR-2001-39, Microsoft Research, 2001.
[24]
H. C. Lauer and R. M. Needham. On the duality of operating system structures. Operating Systems Review, 13(2):3--19, 1979.
[25]
D. Lea. Concurrent Programming in Java. Addison-Wesley, second edition, 2000.
[26]
E. A. Lee. The problem with threads. Technical Report UCB/EECS-2006-1, EECS Department, University of California, Berkeley, January 10 2006.
[27]
P. Li and S. Zdancewic. Combining events and threads for scalable network services: Implementation and evaluation of monadic, application-level concurrency primitives. In PLDI, pages 189--199, June 2007.
[28]
Message Passing Interface Forum. MPI: A message-passing interface standard. http://www.mpi-forum.org.
[29]
R. Milner. A Calculus of Communicating Systems, volume 92 of LNCS. Springer, 1980.
[30]
R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, parts I and II. Technical Report LFCS Report 89-85, University of Edinburgh, June 1989.
[31]
J. K. Ousterhout. Why threads are a bad idea (for most purposes). In Usenix Annual Tech. Conf., 1996. Invited talk.
[32]
D. C. Schmidt, M. Stal, H. Rohnert, and F. Buschmann. Pattern-Oriented Software Architecture: Patterns for Concurrent and Networked Objects. Addison-Wesley, 2000.
[33]
R. Sekar, M. Bendre, D. Dhurjati, and P. Bollineni. A fast automaton-based method for detecting anomalous program behaviors. Security and Privacy, page 144, 2001.
[34]
S. F. Siegel and G. S. Avrunin. Analysis of MPI programs. Technical Report UM-CS-2003-036, University of Massachusetts, 2004.
[35]
F. Smith, D. Walker, and J. G. Morrisett. Alias types. In ESOP, volume 1782 of LNCS, pages 366--381, 2000.
[36]
M. M. Strout, B. Kreaseck, and P. D. Hovland. Data- ow analysis for MPI programs. In ICPP, Aug. 2006.
[37]
R. von Behren, J. Condit, and E. Brewer. Why events are a bad idea (for high-concurrency servers). In HotOS, 2003.
[38]
R. von Behren, J. Condit, F. Zhou, G. C. Necula, and E. Brewer. Capriccio: Scalable threads for internet services. In SOSP, 2003.

Cited By

View all

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
ESEC-FSE '07: Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering
September 2007
638 pages
ISBN:9781595938114
DOI:10.1145/1287624
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 September 2007

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. asynchronous components
  2. concurrency
  3. design for analyzability
  4. event-driven programming
  5. static analysis

Qualifiers

  • Article

Conference

ESEC/FSE07
Sponsor:

Acceptance Rates

Overall Acceptance Rate 112 of 543 submissions, 21%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)4
  • Downloads (Last 6 weeks)2
Reflects downloads up to 20 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2014)Automatic verification of active device driversACM SIGOPS Operating Systems Review10.1145/2626401.262642448:1(106-118)Online publication date: 15-May-2014
  • (2012)Automatic Verification of Message-Based Device DriversElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.102.3102(4-17)Online publication date: 26-Nov-2012
  • (2011)ACACM SIGPLAN Notices10.1145/2076021.204813446:10(903-920)Online publication date: 22-Oct-2011
  • (2011)ACProceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications10.1145/2048066.2048134(903-920)Online publication date: 22-Oct-2011
  • (2011)Composable asynchronous eventsProceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/1993498.1993572(628-639)Online publication date: 4-Jun-2011
  • (2011)Composable asynchronous eventsACM SIGPLAN Notices10.1145/1993316.199357246:6(628-639)Online publication date: 4-Jun-2011
  • (2011)FlowTalkIEEE Transactions on Software Engineering10.1109/TSE.2010.6637:4(526-543)Online publication date: 1-Jul-2011
  • (2010)The case for active device driversProceedings of the first ACM asia-pacific workshop on Workshop on systems10.1145/1851276.1851283(25-30)Online publication date: 30-Aug-2010
  • (2010)Automatic Concurrency Management for distributed applicationsProceedings of the The IEEE symposium on Computers and Communications10.1109/ISCC.2010.5546705(589-594)Online publication date: 22-Jun-2010
  • (2010)The composability problem of events and threads in distributed systems2010 2nd International Conference on Education Technology and Computer10.1109/ICETC.2010.5529673(V4-311-V4-315)Online publication date: Jun-2010
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media