The ARRAY series of workshops explores:
The goal of the workshop is to share knowledge about how to use and modify Infer in industrial and academic contexts.
This symposium seeks to bring together programming language and machine learning communities to encourage collaboration and exploration in the areas of mutual benefit. The symposium will include a combination of rigorous peer-reviewed papers and invited events. The symposium will seek papers on a diverse range of topics related to programming languages and machine learning including (and not limited to):
Workshop topics include (but are not limited to):
Static and dynamic analysis techniques and tools for Java, and other programming languages, have received widespread attention for a long time. The application domains of these analyses range from core libraries to modern technologies such as web services and Android applications. Over time, various analysis frameworks have been developed to provide techniques for optimizing programs, ensuring code quality, and assessing security and compliance.
SOAP 2021 aims to bring together the members of the program analysis community to share new developments and shape new innovations in program analysis. For SOAP 2021, we invite contributions and inspirations from researchers and practitioners working with program analysis. We are particularly interested in exciting analysis framework ideas, innovative designs, and analysis techniques, including preliminary results of work in progress. We will also focus on the state of the practice for program analysis by encouraging submissions by industrial participants, including tool demonstration submissions. The workshop agenda will continue its tradition of lively discussions on extensions of existing frameworks, development of new analyses and tools, and how program analysis is used in real-world scenarios.
Emerging non-volatile memory (NVM) technologies provide fast access to persistent data (guaranteed to endure power failures/crashes) at a performance comparable to volatile memory (RAM). NVM (a.k.a. persistent memory) is believed to supplant RAM in the near future, leading to substantial changes in software and its engineering.
However, the performance gains of NVM are difficult to exploit correctly. A key challenge lies in ensuring correct recovery after a crash by maintaining the consistency of the data in persistent memory. This requires an understanding of the underlying (weak) persistency model, describing the order in which stores are propagated to NVM. The problem is that CPUs are not directly connected to memory; instead there are multiple non-persistent caches in between. Consequently, memory stores are not propagated to NVM at the time and in the order issued by the processor, but rather at a later time and in the order decided by cache coherence protocols.
In this tutorial, we demonstrate three facets of persistency research:
We present the formal persistency semantics of the ubiquitous Intel-x86 and ARMv8 CPU architectures.
We describe common programming patterns for implementing higher-level persistent libraries (e.g. transactions).
We present persistent linearisability as a correctness condition for verifying persistent algorithms.
OpenMP is an industry-standard API for writing portable shared-memory parallel programs in C/C++/Fortran. Almost every mainstream compiler of these languages now supports compilation of OpenMP programs. However, we are not aware of any compiler framework which was designed from the ground up taking OpenMP semantics into account. Consequently, not all components of such frameworks are generally applicable (or conforming) to OpenMP parallel semantics. This half-day tutorial presents a new open-source source-to-source compiler framework called IMOP (IIT Madras OpenMP compiler), which addresses such limitations.
Each component in IMOP has been designed and implemented by taking OpenMP syntax and semantics into account. IMOP comprises of more than 154 kLOC in Java, and works on OpenMP C programs as its input. With its numerous unique features such as OpenMP-aware compilation, automatic generation of parallel variants of the serial data-flow passes, self-stabilization of program abstractions under program modifications, integration with the Z3 SMT solver, and so on, IMOP can significantly simplify the task of writing tools for program analysis, profiling, and optimizations. In this hands-on tutorial, we will teach the fundamentals and certain advanced concepts of IMOP to the participants, which can help them in the faster development of their research prototypes.
The tutorial will briefly cover the following:
Setting up the Gigahorse framework development environment and related toolchains
Specifying simple program analyses
Implement analyses for known vulnerabilities such as reentrancy
Run these analyses at scale, and compare their results
Introduce basic analysis design considerations and their effect on precision, completeness and scalability
Necessary background: the tutorial will make as few assumptions as possible regarding the background of participants, especially relative to the blockchain and smart contracts. Necessary concepts of smart contract execution will be introduced in the tutorial, although the emphasis will be on static analysis. Participants should have some background in intermediate languages and simple program analysis, at the level of a Compilers course.
Medium: There will be an initial presentation of tutorial material (slides + screen sharing for command line and setup). Afterwards, the tutorial is expected to be interactive, with extensive screen sharing among participants to jointly examine code.
Platform: Participants should have machines with a Unix-like OS (Linux preferred, MacOS should be ok). The Souffle language will be ideally installed and tested before the tutorial.