MapReduce framework for data-parallel computation was first proposed by Google and later implemented in the Apache Hadoop project. Under the MapReduce framework, a reducer computes output values from a sequence of input values transmitted over the network. Due to the non-determinism in data transmission, the order of input values arrives at the reducer is not fixed. The commutativity problem of reducers asks if the output of a reducer is independent of the order of its inputs. There are several advantages for a reducer being commutative, e.g., the verification problem of a MapReduce program can be reduced to the problem of verifying a sequential program. In this paper, we present a tool J-ReCoVer (Java Reducer Commutativity Verifier) that implements effective heuristics for reducer commutativity analysis. J-ReCoVer is the first tool that is specialized in checking reducer commutativity. Experimental results over 118 benchmark examples collected from open repositories are very positive; J-ReCoVer correctly handles over 97% of them.
Tue 3 DecDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
15:30 - 17:15 | VerificationResearch Papers at Bali Room Chair(s): Zhilin Wu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences | ||
15:30 15mTalk | J-ReCoVer: Java Reducer Commutativity Verifier [Tool Paper] Research Papers Yu-Fang Chen Academia Sinica, Chang-Yi Chiang Graduate Institute of Information Management, National Taipei University, Taiwan, Lukáš Holík Brno University of Technology, Wei-Tsung Kao Institute of Information Science, Academia Sinica, Taiwan, Hsin-Hung Lin Institute of Information Science, Academia Sinica, Taiwan, Yean-Fu Wen Graduate Institute of Information Management, National Taipei University, Taiwan, Tomáš Vojnar Brno University of Technology, Wei-Cheng Wu Institute of Information Science, Academia Sinica, Taiwan | ||
15:45 30mTalk | Uniform Random Process Model Revisited Research Papers Wenbo Zhang , Huan Long Shanghai Jiao Tong University, Xian Xu East China University of Science and Technology | ||
16:15 30mTalk | Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions Research Papers Makoto Tatsuta National Institute of Informatics, Koji Nakazawa Graduate School of Informatics, Nagoya University, Daisuke Kimura Toho University | ||
16:45 30mTalk | Compositional Verification of Heap-Manipulating Programs through Property-Guided Learning Research Papers Long H. Pham Singapore University of Technology and Design, Jun Sun Singapore Management University, Singapore, Quang Loc Le Teesside University | ||