Abhishek Udupa
ABSTRACT
With the maturing of technology for model checking and constraint solving, there is an emerging opportunity to develop programming tools that can transform the way systems are specified. In this paper, we propose a new way to program distributed protocols using concolic snippets. Concolic snippets are sample execution fragments that contain both concrete and symbolic values. The proposed approach allows the programmer to describe the desired system partially using the traditional model of communicating extended finite-state-machines (EFSM), along with high-level invariants and concrete execution fragments. Our synthesis engine completes an EFSM skeleton by inferring guards and updates from the given fragments which is then automatically analyzed using a model checker with respect to the desired invariants. The counterexamples produced by the model checker can then be used by the programmer to add new concrete execution fragments that describe the correct behavior in the specific scenario corresponding to the counterexample.
We describe TRANSIT, a language and prototype implementation of the proposed specification methodology for distributed protocols. Experimental evaluations of TRANSIT to specify cache coherence protocols show that (1) the algorithm for expression inference from concolic snippets can synthesize expressions of size 15 involving typical operators over commonly occurring types, (2) for a classical directory-based protocol, TRANSIT automatically generates, in a few seconds, a complete implementation from a specification consisting of the EFSM structure and a few concrete examples for every transition, and (3) a published partial description of the SGI Origin cache coherence protocol maps directly to symbolic examples and leads to a complete implementation in a few iterations, with the programmer correcting counterexamples resulting from underspecified transitions by adding concrete examples in each iteration.
- Intel Core2 Extreme Processor X6800 and Intel Core2 Duo Desktop Processor E6000 and E4000 Sequence -- Specification Update, 2003. URL http://www.intel.com/design/processor/ specupdt/313279.htm.Google Scholar
- D. Abts, D. J. Lilja, and S. Scott. So Many States, So Little Time: Verifying Memory Coherence in the Cray X1. In Proceedings of the International Parallel and Distributed Processing Symposium, IPDPS '03, pages 1--11, 2003. Google ScholarDigital Library
- E. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. .Long, K. McMillan, and L. Ness. Verification of the Futurebus+ Cache Coherence Protocol. Formal Methods in System Design, 6:217--232, 1995. Google ScholarDigital Library
- N. Dave, M. C. Ng, and Arvind. Automatic Synthesis of Cache- Coherence Protocol Processors Using Bluespec. In Formal Methods and Models for Codesign, MEMOCODE '05, pages 25--34, 2005. Google ScholarDigital Library
- D. Dill, A. Drexler, A. Hu, and C. Yang. Protocol Verification as a Hardware Design Aid. In Proceedings of the International Conference on Computer Design, ICCD '92, pages 522--525, 1992. Google ScholarDigital Library
- B. Finkbeiner and S. Jacobs. Lazy Synthesis. In 13th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI '12, LNCS 7148, pages 219--234, 2012. Google ScholarDigital Library
- S. Gulwani. Automating String Processing in Spreadsheets using Input-output Examples. In Proceedings of The 38th ACM SIGPLAN/ SIGACT Symposium on Principles of Programming Languages, POPL '11, pages 317--330, 2011. Google ScholarDigital Library
- S. Gulwani, S. Jha, A. Tiwari, and R. Venkatesan. Synthesis of Loopfree Programs. In Proceedings of the 32nd ACM SIGPLAN conference on Programming Language Design and Implementation, PLDI '11, pages 62--73, 2011. Google ScholarDigital Library
- D. Harel. Can Programming Be Liberated, Period? IEEE Computer, 41(1):28--37, Jan. 2008. Google ScholarDigital Library
- D. Harel and R. Marelly. Come, Let's Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer-Verlag New York, 2003. Google ScholarDigital Library
- D. Harel, A. Marron, and G. Weiss. Behavioral Programming. Communications of the ACM, 55(7):90--100, Jul. 2012. Google ScholarDigital Library
- G. J. Holzmann. The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, 2003. Google ScholarDigital Library
- S. Jha, S. Gulwani, S. A. Seshia, and A. Tiwari. Oracle-guided Component-based Program Synthesis. In Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - Volume 1, ICSE '10, pages 215--224, 2010. Google ScholarDigital Library
- G. Katz and D. Peled. MCGP: A Software Synthesis Tool Based on Model Checking and Genetic Programming. In 8th Internation Symposium on Automated Technology for Verification and Analysis, ATVA '10, LNCS 6252, pages 359--364, 2010. Google ScholarDigital Library
- V. Kuncak, M. Mayer, R. Piskac, and P. Suter. Software Synthesis Procedures. Communications of the ACM, 55(2):103--111, Feb. 2012. Google ScholarDigital Library
- J. Laudon and D. Lenoski. The SGI Origin: A ccNUMA Highly Scalable Server. In Proceedings of the 24th Annual International Symposium on Computer Architecture, ISCA '97, pages 241--251, 1997. Google ScholarDigital Library
- N. A. Lynch. Distributed algorithms. Morgan Kaufmann Publishers Inc., 1996. Google ScholarDigital Library
- M. M. K. Martin, D. J. Sorin, B. M. Beckmann, M. R. Marty, M. Xu, A. R. Alameldeen, K. E. Moore, M. D. Hill, and D. A. Wood. Multifacet's General Execution-driven Multiprocessor Simulator (GEMS) Toolset. SIGARCH Computer Architecture News, 33(4):92--99, Nov. 2005. Google ScholarDigital Library
- L. D. Moura and N. Bjørner. Z3: An Efficient SMT Solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS '08, pages 337--340, 2008. Google ScholarDigital Library
- K. Sen, D. Marinov, and G. Agha. CUTE: A Concolic Unit Testing Engine for C. In Proceedings of the 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE '05, pages 263--272, 2005. Google ScholarDigital Library
- S. A. Seshia. Sciduction: Combining Induction, Deduction, and Structure for Verification and Synthesis. In Proceedings of the 49th Annual Design Automation Conference, DAC '12, pages 356--365, 2012. Google ScholarDigital Library
- R. Singh and A. Solar-Lezama. Synthesizing Data Structure Manipulations from Storyboards. In Proceedings of the 19th ACM Symposiumon Foundations of Software Engineering, FSE '11, pages 289--299,2011. Google ScholarDigital Library
- A. Solar-Lezama, R. Rabbah, R. Bodik, and K. Ebcioglu. Programming by Sketching for Bitstreaming Programs. In Proceedings of the SIGPLAN 2005 Conference on Programming Language Design and Implementation, PLDI '05, pages 281--294, 2005. Google ScholarDigital Library
- A. Solar-Lezama, C. G. Jones, and R. Bodik. Sketching Concurrent Data Structures. In Proceedings of the SIGPLAN 2008 Conference on Programming Language Design and Implementation, PLDI '08, pages 136--148, 2008. Google ScholarDigital Library
- D. J. Sorin, M. D. Hill, and D. A. Wood. A Primer on Memory Consistency and Cache Coherence. Morgan Claypool, 2011. Google ScholarDigital Library
- S. Srivastava, S. Gulwani, and J. S. Foster. From Program Verification to Program Synthesis. In Proceedings of the 37th annual ACM Symposium on Principles of Programming Languages, POPL '10, pages 313--326, 2010. Google ScholarDigital Library
- M. Talupur and M. R. Tuttle. Going with the Flow: Parameterized Verification using Flows: An Industrial Experience. In Proceedings of the 2008 Internation Conference on Formal Methods in Computer- Aided Design, FMCAD '08, pages 1--8, 2008. Google ScholarDigital Library
- W. Thomas. Facets of Synthesis: Revisiting Church's Problem. In Foundations of Software Science and Computational Structures, 12th International Conference, FOSSACS '09, LNCS 5504, pages 1--14, 2009. Google ScholarDigital Library
Index Terms
- TRANSIT: specifying protocols with concolic snippets
Recommendations
TRANSIT: specifying protocols with concolic snippets
PLDI '13With the maturing of technology for model checking and constraint solving, there is an emerging opportunity to develop programming tools that can transform the way systems are specified. In this paper, we propose a new way to program distributed ...
Boosting performance of directory-based cache coherence protocols with coherence bypass at subpage granularity and a novel on-chip page table
CF '16: Proceedings of the ACM International Conference on Computing FrontiersChip multiprocessors (CMPs) require effective cache coherence protocols as well as fast virtual-to-physical address translation mechanisms for high performance. Directory-based cache coherence protocols are the state-of-the-art approaches in many-core ...
Increasing the effectiveness of directory caches by deactivating coherence for private memory blocks
ISCA '11: Proceedings of the 38th annual international symposium on Computer architectureTo meet the demand for more powerful high-performance shared-memory servers, multiprocessor systems must incorporate efficient and scalable cache coherence protocols, such as those based on directory caches. However, the limited directory cache size of ...
Comments