MapReduce framework for data-parallel computation was ﬁrst 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 ﬁxed. 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 veriﬁcation 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 Dec Times are displayed in time zone: Beijing, Chongqing, Hong Kong, Urumqi change
15:30 - 17:15
|J-ReCoVer: Java Reducer Commutativity Veriﬁer [Tool Paper]|
Yu-Fang ChenAcademia Sinica, Chang-Yi ChiangGraduate Institute of Information Management, National Taipei University, Taiwan, Lukáš HolíkBrno University of Technology, Wei-Tsung KaoInstitute of Information Science, Academia Sinica, Taiwan, Hsin-Hung LinInstitute of Information Science, Academia Sinica, Taiwan, Yean-Fu WenGraduate Institute of Information Management, National Taipei University, Taiwan, Tomáš VojnarBrno University of Technology, Wei-Cheng WuInstitute of Information Science, Academia Sinica, Taiwan
|Uniform Random Process Model Revisited|
|Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions|
|Compositional Verification of Heap-Manipulating Programs through Property-Guided Learning|