State Exploration of Scala Actor Programs by Mirco Dotta BSc., Computer Science ´ Ecole Polytechnique F´ed´erale de Lausanne (2006) Submitted to the School of Computer and Communication Sciences in partial fulfillment of the requirements for the degree of Master of Science in Computer Science at the ´ ´ ´ ECOLE POLYTECHNIQUE FEDERALE DE LAUSANNE March 2009 (cid:13)c Mirco Dotta, MMIX. All rights reserved. The author hereby grants to EPFL permission to reproduce and distribute publicly paper and electronic copies of this thesis document in whole or in part. Author .............................................................. School of Computer and Communication Sciences March 13, 2009 To my mother, Giusy. State Exploration of Scala Actor Programs by Mirco Dotta Submitted to the School of Computer and Communication Sciences on March 13, 2009, in partial fulfillment of the requirements for the degree of Master of Science in Computer Science Abstract The growing use of multicore and networked computing systems is increasing the im- portance of developing reliable parallel and distributed code. Unfortunately, develop- ing and testing such code is notoriously hard, especially for shared-memory models of programming. The actor model offers a promising alternative paradigm based on message passing. Essentially, an actor is an autonomous concurrent object which interacts with other actors only by exchanging messages. In actor-based systems, the key source of non-determinism is the order in which messages are delivered to—and processed by—the actors. Bugs can still occur in actor programs as the interleaving of messages may be incorrect, or the sequential code within an actor can have bugs. We developed a general framework, called SEJAP, for exploring possible message schedules in actor systems compiled to the Java bytecode. Specifically, in this dis- sertation, we present one instantiation of SEJAP for the actor library of the Scala programming language. To the best of our knowledge, this is the first framework that allows systematic exploration of Scala actor programs. We also present two optimiza- tions that alleviate the state explosion problem typical for such exploration, and thus speed up the overall exploration of actor programs in SEJAP. We have implemented our framework, Scala instantiation, and optimizations in Java PathFinder, a widely used model checker for Java bytecode developed by NASA. Preliminary results show that SEJAP can effectively explore executions of actor programs. Further, our use of SEJAP already discovered a previously unknown bug in the sample code from a popular site for Scala. Thesis Supervisor: Viktor Kuncak Title: Assistant Professor External Thesis Supervisor: Darko Marinov Title: Assistant Professor i ii Acknowledgements I would like to express my gratitude to my advisor here at UIUC, Darko Marinov, for accepting me as a visiting student in his group, for giving me the freedom of pursuing my personal research interests and for providing me tremendous support throughout this unique experience. I’m also grateful to my advisor at EPFL, Viktor Kuncak, for giving me the op- portunity to come to UIUC to carry out my research and for his continuous support from EPFL. I was very fortunate in meeting Viktor during my first year of Master studies at EPFL. I thank him for believing in me ever since we met and for pushing me to learn the many nuances of software verification. I’m greatly thankful to Steven (Steve) Lauterburg—a PhD student in Darko’s group—with whom I worked very closely during my entire visit at UIUC. Many of the ideas presented in this dissertation have in fact been the realization of this collaboration. Steve spent a lot of time in discussing various issues with me, pair programming SEJAP, and providing many valuable comments about several draft versions of this dissertation. I wish him the very best of luck with his work and life. I also would like to thank Yun-young Lee, with whom I shared an office, for making every working day enjoyable. Besides being a wonderful friend, her baking skills were a valuable source of energy during the night and weekends spent working on this research. I would like to thank professor Gul Agha for the many fruitful discussions on the actor model, and for giving me the opportunity to audit his class which has greatly helped me in realizing this work. I also would like to sincerely express my gratitude to Philipp Haller for his constant availability and dedication in answering the many iii questions I had on the semantics of actors in Scala. I’m also deeply grateful to C´edric Jeanneret for providing me with comments and criticisms that helped improve the quality of this dissertation. I would like to thank professor Ralph Johnson for finding the time to personally discuss several software engineering topics and for giving me the opportunity to audit hisclassonobject-oriented programminganddesign. I’malsogratefultoSenKoushik for meeting with me during my brief visit at UC Berkeley, and sharing his vision on the area of automatic software testing. There are many extraordinary individuals whom I have met in my life and that have shaped me into the person I am today. Due to the lack of space I cannot mention everyone here but you all are in my heart and memories. Nicola Ermotti and Samuele Gantner have played fundamental roles in my growth, I will never be able to express the real extent of my gratitude. Samuele also provided an incredible number of comments on this dissertation, I owe him a big thanks. Also thanks to my fellow “blogger-friends” who supported me constantly during this adventure abroad. Thanks to Martina B¨orner, Claudia Comin, Stefano Giordano, Guy Mu¨ller, Gisella Pfund, Dario Poggiali, and Luca Sulmoni. Without you my life would not be as much fun. Last but not least, I would like to thank my family for their unconditional love, support, encouragement, and patience. This work is dedicated to them. iv Table of Contents 1 Introduction 1 1.1 Problem Statement . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.2 Proposed Solution and Contributions . . . . . . . . . . . . . . . . . . 4 1.3 Organization of this Dissertation . . . . . . . . . . . . . . . . . . . . 5 2 Background 7 2.1 The Actor Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.1.1 Actors in a Nutshell . . . . . . . . . . . . . . . . . . . . . . . 7 2.1.2 Actor Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.2 The Scala Programming Language . . . . . . . . . . . . . . . . . . . 10 2.2.1 Scala in Brief . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.2.2 Pattern Matching . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.2.3 Actors by Examples . . . . . . . . . . . . . . . . . . . . . . . 11 2.2.4 Impurities of the Library . . . . . . . . . . . . . . . . . . . . . 14 2.2.5 Actor Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.3 Java PathFinder . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.3.1 A Model Checker for Java Bytecode . . . . . . . . . . . . . . . 17 2.3.2 JPF Architecture and Design . . . . . . . . . . . . . . . . . . 18 3 Example 21 3.1 A Simple Client-Server Program . . . . . . . . . . . . . . . . . . . . . 21 3.2 Description of the Space Exploration . . . . . . . . . . . . . . . . . . 24 4 Framework 27 4.1 Actor States . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 4.2 Actor Execution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 4.3 Message Management . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 4.4 Exploration Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . 30 4.5 Library Instantiation . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 v 4.5.1 Binding a Concrete Actor Library to the Framework . . . . . 32 4.5.2 Adapting the Library Interface . . . . . . . . . . . . . . . . . 34 5 Optimizations 37 5.1 State Comparison . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 5.2 Step Granularity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 6 Implementation 41 6.1 System Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 6.2 Java PathFinder Modifications . . . . . . . . . . . . . . . . . . . . . . 42 6.3 Java PathFinder and Scala . . . . . . . . . . . . . . . . . . . . . . . . 44 6.4 Adapting the Scala Actor Library . . . . . . . . . . . . . . . . . . . . 46 7 Evaluation 49 7.1 Optimized Thread Context Switching . . . . . . . . . . . . . . . . . . 50 7.2 Subjects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 7.3 State Comparison . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 7.4 Step Granularity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 8 Related Work 55 9 Conclusions 59 9.1 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 A Original Client-Server ScalaWiki Code 63 vi