Write a Blog >>
Wed 12 Oct 2022 16:30 - 16:50 at Gold A - Technical Session 20 - Web, Cloud, Networking Chair(s): Karine Even-Mendoza

Communication nondeterminism is one of the main reasons for the intractability of verification of message passing concurrency. In many practical message passing programs, the non-deterministic communication structure is symmetric and decomposed into epochs to obtain efficiency. Thus, symmetries and epoch structure can be exploited to reduce verification complexity. In this paper, we present a dynamic-symbolic runtime verification technique for single-path MPI programs, which (i) exploits communication symmetries by way of specifying symmetry breaking predicates (SBP) and (ii) performs compositional verification based on epochs. On the one hand, SBPs prevent the symbolic decision procedure from exploring isomorphic parts of the search space, and on the other hand, epochs restrict the size of a program needed to be analyzed at a point in time. We show that our analysis is sound and complete for single-path MPI programs on a given input. We further demonstrate that our approach leads to (i) a significant reduction in verification times and (ii) scaling up to larger benchmark sizes compared to prior trace verifiers.

Wed 12 Oct

Displayed time zone: Eastern Time (US & Canada) change

16:00 - 18:00
Technical Session 20 - Web, Cloud, NetworkingJournal-first Papers / Late Breaking Results / Research Papers / Tool Demonstrations / Industry Showcase at Gold A
Chair(s): Karine Even-Mendoza Imperial College London
16:00
20m
Paper
Mutation-based Analysis of Queueing Network Performance Models -- Journal First Research
Journal-first Papers
Thomas Laurent Lero & University College Dublin, Paolo Arcaini National Institute of Informatics , Catia Trubiani Gran Sasso Science Institute, Anthony Ventresque University College Dublin & Lero, Ireland
Link to publication DOI
16:20
10m
Demonstration
WebMonitor: https://youtu.be/hqVw0JU3k9c
Tool Demonstrations
Ennio Visconti TU Wien, Christos Tsigkanos University of Bern, Switzerland, Laura Nenzi University of Trieste
16:30
20m
Research paper
Exploiting Epochs and Symmetries in Analysing MPI Programs
Research Papers
Rishabh Ranjan IIT Delhi, Ishita Agrawal IIT Delhi, Subodh Sharma IIT Delhi
16:50
20m
Paper
MLASP: Machine learning assisted capacity planning
Journal-first Papers
Arthur Vitui Concordia University, Tse-Hsun (Peter) Chen Concordia University
Link to publication DOI
17:10
20m
Research paper
Graph based Incident Extraction and Diagnosis in Large-Scale Online SystemsVirtual
Research Papers
Zilong He Sun Yat-Sen University, Pengfei Chen Sun Yat-Sen University, Yu Luo Tencent Inc., Qiuyu Yan Tencent Inc., Hongyang Chen School of Computer Science and Engineering, Sun Yat-sen University, Guangba  Yu Sun Yat-Sen University, Fangyuan Li Tencent Inc.
17:30
10m
Paper
ESAVE: Estimating Server and Virtual Machine EnergyVirtual
Late Breaking Results
Priyavanshi Pathania Accenture Labs, Rohit Mehra Accenture Labs, Vibhu Saujanya Sharma Accenture Labs, Vikrant Kaulgud Accenture Labs, India, Sanjay Podder Accenture, Adam P. Burden Accenture
17:40
20m
Industry talk
MCDA Framework for Edge-Aware Multi-Cloud Hybrid Architecture RecommendationVirtual
Industry Showcase
Manish Ahuja Accenture Labs, Narendranath Sukhavasi Accenture Labs, Swapnajeet Choudhury Accenture Labs, Kaushik Amar Das Accenture Labs, Kapil Singi Accenture, Kuntal Dey Accenture Labs, India, Vikrant Kaulgud Accenture Labs, India