tutorial

Synthesis of Synchronization using Uninterpreted Functions

Authors:

Roderick Bloem,

Georg Hofferek,

Bettina Könighofer,

Robert Könighofer,

Simon Außerlechner,

Raphael SpörkAuthors Info & Claims

FMCAD '14: Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design

Pages 35 - 42

Published: 21 October 2014 Publication History

Abstract

Correctness of a program with respect to concurrency is often hard to achieve, but easy to specify: the concurrent program should produce the same results as a sequential reference version. We show how to automatically insert small atomic sections into a program to ensure correctness with respect to this implicit specification. Using techniques from bounded software model checking, we transform the program into an SMT formula that becomes unsatisfiable when we add correct atomic sections. By using uninterpreted functions to abstract data-related computational details, we make our approach applicable to programs with very complex computations, e.g., cryptographic algorithms. Our method starts with an empty set of atomic sections, and, based on counterexamples obtained from the SMT solver, refines the program by adding new atomic sections until correctness is achieved. We compare two different such refinement methods and provide experimental results, including Linux kernel modules where we successfully fix race conditions.

References

[1]

L. Bachmair, I. V. Ramakrishnan, A. Tiwari, and L. Vigneron. Congruence closure modulo associativity and commutativity. In FroCoS'00, LNCS 1794, 2000.

Digital Library

[2]

R. Bloem, R. Drechsler, G. Fey, A. Finder, G. Hofferek, R. Könighofer, J. Raik, U. Repinski, and A. Sülflow. FoREnSiC - an automatic debugging environment for C programs. In HVC'12, LNCS 7857. Springer, 2012.

Digital Library

[3]

R. E. Bryant, S. M. German, and M. N. Velev. Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. ACM Trans. Comput. Log., 2(1):93--134, 2001.

Digital Library

[4]

J. R. Burch and D. L. Dill. Automatic verification of pipelined microprocessor control. In CAV'94, LNCS 818. Springer, 1994.

Digital Library

[5]

P. Cerný, T. A. Henzinger, A. Radhakrishna, L. Ryzhyk, and T. Tarrach. Efficient synthesis for concurrency by semantics-preserving transformations. In CAV'13, LNCS 8044. Springer, 2013.

Digital Library

[6]

S. Cherem, T. M. Chilimbi, and S. Gulwani. Inferring locks for atomic sections. In PLDI'08. ACM, 2008.

Digital Library

[7]

E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs. Springer, 1981.

Digital Library

[8]

E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst., 8(2):244--263, 1986.

Digital Library

[9]

E. M. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In TACAS'04, LNCS 2988. Springer, 2004.

[10]

E. Cohen, M. Dahlweid, M. A. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, and S. Tobies. VCC: A practical system for verifying concurrent C. In TPHOLs'09, LNCS 5674. Springer, 2009.

Digital Library

[11]

L. Cordeiro and B. Fischer. Verifying multi-threaded software using SMT-based context-bounded model checking. In ICSE'11. ACM, 2011.

Digital Library

[12]

L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS'08, 2008.

Digital Library

[13]

E. Farchi, Y. Nir, and S. Ur. Concurrent bug patterns and how to test them. In IPDPS'03. IEEE, 2003.

Digital Library

[14]

M. K. Ganai and A. Gupta. Efficient modeling of concurrent systems in BMC. In SPIN'08, LNCS 5156. Springer, 2008.

Digital Library

[15]

G. Hofferek and R. Bloem. Controller synthesis for pipelined circuits using uninterpreted functions. In MEMOCODE'11. IEEE, 2011.

Digital Library

[16]

G. Hofferek, A. Gupta, B. Könighofer, J.-H. R. Jiang, and R. Bloem. Synthesizing multiple boolean functions using interpolation on a single proof. In FMCAD'13. IEEE, 2013.

[17]

U. Junker. Quickxplain: Preferred explanations and relaxations for over-constrained problems. In AAAI'04. AAAI Press / The MIT Press, 2004.

Digital Library

[18]

V. Kahlon. Automatic lock insertion in concurrent programs. In FMCAD'12. IEEE, 2012.

[19]

A. Menezes, P. C. van Oorschot, and S. A. Vanstone. Handbook of Applied Cryptography. CRC Press, 1996.

Digital Library

[20]

A. Pnueli, O. Strichman, and M. Siegel. The code validation tool CVT: Automatic verification of a compilation process. STTT, 2(2):192--201, 1998.

[21]

I. Rabinovitz and O. Grumberg. Bounded model checking of concurrent programs. In CAV'05, LNCS 3576. Springer, 2005.

Digital Library

[22]

R. Reiter. A theory of diagnosis from first principles. Artif. Intell, 32(1), 1987.

Digital Library

[23]

A. Solar-Lezama, C. G. Jones, and R. Bodík. Sketching concurrent data structures. In PLDI'08. ACM, 2008.

Digital Library

[24]

M. T. Vechev, E. Yahav, and G. Yorsh. Abstraction-guided synthesis of synchronization. In POPL'10. ACM, 2010.

Digital Library

Cited By

Houshmand FLesani MVora K(2021)Grafs: declarative graph analyticsProceedings of the ACM on Programming Languages10.1145/34735885:ICFP(1-32)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473588
Sung CLahiri SEnea CWang CHuchard MKästner CFraser G(2018)Datalog-based scalable semantic diffing of concurrent programsProceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering10.1145/3238147.3238211(656-666)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3238147.3238211
Černý PClarke EHenzinger TRadhakrishna ARyzhyk LSamanta RTarrach T(2017)From non-preemptive to preemptive scheduling using synchronization synthesisFormal Methods in System Design10.1007/s10703-016-0256-550:2-3(97-139)Online publication date: 1-Jun-2017
https://dl.acm.org/doi/10.1007/s10703-016-0256-5
Show More Cited By

Index Terms

Synthesis of Synchronization using Uninterpreted Functions
1. Applied computing
  1. Arts and humanities
    1. Architecture (buildings)
      1. Computer-aided design
  2. Physical sciences and engineering
    1. Engineering
      1. Computer-aided design
2. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Contextual software domains
      1. Operating systems
        Process management
        Process synchronization
    2. Software functional properties
      1. Formal methods

Recommendations

Abstraction-guided synthesis of synchronization

We present a novel framework for automatic inference of efficient synchronization in concurrent programs, a task known to be difficult and error-prone when done manually. Our framework is based on abstract interpretation and can infer synchronization ...
Abstraction-guided synthesis of synchronization
POPL '10

We present a novel framework for automatic inference of efficient synchronization in concurrent programs, a task known to be difficult and error-prone when done manually.

Our framework is based on abstract interpretation and can infer synchronization ...
Trace Abstraction-Based Verification for Uninterpreted Programs
Formal Methods
Abstract
The verification of uninterpreted programs is undecidable in general. This paper proposes to employ counterexample-guided abstraction refinement (CEGAR) framework for verifying uninterpreted programs. Different from the existing interpolant-based ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

FMCAD '14: Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design

October 2014

219 pages

ISBN:9780983567844

Editors:
Koen Claessen,
Viktor Kuncak,
Publications Chair:
Barbara Jobstmann

Sponsors

FMCAD: FMCAD, Inc

In-Cooperation

Publisher

FMCAD Inc

Austin, Texas

Publication History

Published: 21 October 2014

Check for updates

Qualifiers

Tutorial
Research
Refereed limited

Conference

FMCAD '14

Sponsor:

FMCAD

FMCAD '14: Formal Methods in Computer-Aided Design

October 21 - 24, 2014

Lausanne, Switzerland

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
39
Total Downloads

Downloads (Last 12 months)3
Downloads (Last 6 weeks)0

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Houshmand FLesani MVora K(2021)Grafs: declarative graph analyticsProceedings of the ACM on Programming Languages10.1145/34735885:ICFP(1-32)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473588
Sung CLahiri SEnea CWang CHuchard MKästner CFraser G(2018)Datalog-based scalable semantic diffing of concurrent programsProceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering10.1145/3238147.3238211(656-666)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3238147.3238211
Černý PClarke EHenzinger TRadhakrishna ARyzhyk LSamanta RTarrach T(2017)From non-preemptive to preemptive scheduling using synchronization synthesisFormal Methods in System Design10.1007/s10703-016-0256-550:2-3(97-139)Online publication date: 1-Jun-2017
https://dl.acm.org/doi/10.1007/s10703-016-0256-5
Fowze FYavuz TTalpin J(2016)Specification, verification, and synthesis using extended state machines with callbacksProceedings of the 14th ACM-IEEE International Conference on Formal Methods and Models for System Design10.5555/3343414.3343428(95-104)Online publication date: 18-Nov-2016
https://dl.acm.org/doi/10.5555/3343414.3343428
Khoshnood SKusano MWang CYoung MXie T(2015)ConcBugAssist: constraint solving for diagnosis and repair of concurrency bugsProceedings of the 2015 International Symposium on Software Testing and Analysis10.1145/2771783.2771798(165-176)Online publication date: 13-Jul-2015
https://dl.acm.org/doi/10.1145/2771783.2771798

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents