Presentation: Workshop on the occassion of the defence of Saeed Darabi

When: March 2, 2018, 13:30 - March 3, 2018, 16:00

Where: Ravelijn 1315

Who: 3 speakers

Workshop on the occasion of the defence of Saeed Darabi on Friday March 2^nd, 2018.

Time: 13:30 – 16:00

Location: Ravelijn 1315

Three members of the defence committee will give a presentation:

Ganesh Gopalakrishnan, University of Utah, USA

13:30 – 14:15

Title: Sword: A Bounded Memory-Overhead Detector of OpenMP Data Races in Production Runs (to appear in IPDPS, May 2018, Vancouver, CA)

Abstract:

The detection and elimination of data races in large-scale OpenMP programs is of critical importance. Unfortunately, today's state-of-the-art OpenMP race checkers suffer from high memory overheads and/or miss races. In this paper, we present Sword, a data race detector that significantly improves upon these limitations. Sword limits the application slowdown and memory usage by utilizing only a bounded, user-adjustable memory buffer to collect targeted memory accesses. When the buffer fills up, the accesses are compressed and flushed to a file system for later offline analysis. Sword builds on an operational semantics that formally captures the notion of concurrent accesses within OpenMP regions. An offline race checker that is driven by these semantic rules allows Sword to improve upon happens-before techniques that are known to mask races. To make its offline analysis highly efficient and scalable, Sword employs highly efficient self-balancing interval tree-based algorithms. Our experimental results show that Sword is capable of detecting races even within programs that use over 90% of the memory on each compute node. Further, our evaluations show that it matches or exceeds the best available dynamic OpenMP race checker in detection capability while remaining efficient in execution time.

Simone Atzeni, Ganesh Gopalakrishnan, Zvonimir Rakamaric (Univ. of Utah), Ignacio Laguna, Gregory L. Lee, Dong H. Ahn (Lawrence Livermore National Labs)

Peter Müller, ETH Zurich, Switzerland

14:15 – 15:00

Title: Reasoning with Permissions in Viper

Abstract:

Many recent verification techniques use the notion of permissions to verify programs that access resources such as memory. In particular, there are dozens or even hundreds of separation logics and related formalisms that use permissions to reason about side effects, various forms of concurrency, memory management, I/O behavior, and liveness properties. This talk introduces the Viper infrastructure, which provides an intermediate language that can encode a wide range of permission-based verification problems, including recent logics for weak-memory programs. Viper automates verification via two verification backends based on symbolic execution and verification condition generation, respectively.

15:00 – 15:15 coffee

Ana Varbanescu, Delft University of Technology

15:15 – 16:00

Title: On the performance variability of graph processing: the good, the bad, and the ugly.

Abstract:

With the increase in popularity of graphs as an abstract representation of sparse, connected data, graph processing has become a challenge for algorithms, systems, and infrastructure designers. As graphs grow larger and analysis grows more complex, the performance and efficiency of graph processing applications must be maximized.

The main obstacle in achieving these goals is the performance variability of graph processing applications: the algorithm, the dataset, and the platform itself all play an important role in performance. In this talk, we present the magnitude of the problem while studying two simple graph processing algorithms running on GPUs.

We further show how we can use this variability to our advantage: we dynamically select, at runtime, the best performing algorithm for the given dataset and platform. This approach is made possible by a predictive statistical model that captures the correlation between performance and the properties of the input graph.

We conclude that variability, in the case of graph processing, cannot be avoided, but understanding it can lead to more efficient ways to solve graph analysis problems.

	Home > News and Events > Events
<< EEMCS (EWI) Home News and Events » Group Colloquium » Events » In the Media People Research Education Vacancies Intranet Contact	Presentation: Workshop on the occassion of the defence of Saeed Darabi When: March 2, 2018, 13:30 - March 3, 2018, 16:00 Where: Ravelijn 1315 Who: 3 speakers Workshop on the occasion of the defence of Saeed Darabi on Friday March 2^nd, 2018. Time: 13:30 – 16:00 Location: Ravelijn 1315 Three members of the defence committee will give a presentation: Ganesh Gopalakrishnan, University of Utah, USA 13:30 – 14:15 Title: Sword: A Bounded Memory-Overhead Detector of OpenMP Data Races in Production Runs (to appear in IPDPS, May 2018, Vancouver, CA) Abstract: The detection and elimination of data races in large-scale OpenMP programs is of critical importance. Unfortunately, today's state-of-the-art OpenMP race checkers suffer from high memory overheads and/or miss races. In this paper, we present Sword, a data race detector that significantly improves upon these limitations. Sword limits the application slowdown and memory usage by utilizing only a bounded, user-adjustable memory buffer to collect targeted memory accesses. When the buffer fills up, the accesses are compressed and flushed to a file system for later offline analysis. Sword builds on an operational semantics that formally captures the notion of concurrent accesses within OpenMP regions. An offline race checker that is driven by these semantic rules allows Sword to improve upon happens-before techniques that are known to mask races. To make its offline analysis highly efficient and scalable, Sword employs highly efficient self-balancing interval tree-based algorithms. Our experimental results show that Sword is capable of detecting races even within programs that use over 90% of the memory on each compute node. Further, our evaluations show that it matches or exceeds the best available dynamic OpenMP race checker in detection capability while remaining efficient in execution time. Simone Atzeni, Ganesh Gopalakrishnan, Zvonimir Rakamaric (Univ. of Utah), Ignacio Laguna, Gregory L. Lee, Dong H. Ahn (Lawrence Livermore National Labs) Peter Müller, ETH Zurich, Switzerland 14:15 – 15:00 Title: Reasoning with Permissions in Viper Abstract: Many recent verification techniques use the notion of permissions to verify programs that access resources such as memory. In particular, there are dozens or even hundreds of separation logics and related formalisms that use permissions to reason about side effects, various forms of concurrency, memory management, I/O behavior, and liveness properties. This talk introduces the Viper infrastructure, which provides an intermediate language that can encode a wide range of permission-based verification problems, including recent logics for weak-memory programs. Viper automates verification via two verification backends based on symbolic execution and verification condition generation, respectively. 15:00 – 15:15 coffee Ana Varbanescu, Delft University of Technology 15:15 – 16:00 Title: On the performance variability of graph processing: the good, the bad, and the ugly. Abstract: With the increase in popularity of graphs as an abstract representation of sparse, connected data, graph processing has become a challenge for algorithms, systems, and infrastructure designers. As graphs grow larger and analysis grows more complex, the performance and efficiency of graph processing applications must be maximized. The main obstacle in achieving these goals is the performance variability of graph processing applications: the algorithm, the dataset, and the platform itself all play an important role in performance. In this talk, we present the magnitude of the problem while studying two simple graph processing algorithms running on GPUs. We further show how we can use this variability to our advantage: we dynamically select, at runtime, the best performing algorithm for the given dataset and platform. This approach is made possible by a predictive statistical model that captures the correlation between performance and the properties of the input graph. We conclude that variability, in the case of graph processing, cannot be avoided, but understanding it can lead to more efficient ways to solve graph analysis problems.