Data Sharing Analysis for a Database Programming Language via Abstract Interpretation

摘要

This paper presents an experiment in using a formal technique for static program analysis, based on abstract interpretation, in the context of persistent programming languages. The aim of the analysis is to detect opportunities for safe parallelism for transaction operation scheduling. Transaction operations can be safely interleaved when there is no overlapping among their readsets and writesets. A non-standard interpreter performs the analysis. This interpreter, given the text of a transaction and a representation of the data stored in the database, automatically derives in a finite time an approximation of the readset and writeset of the analysed transaction. Information obtained from the non-standard interpretation is provided to the scheduler before beginning the execution of transaction operations. In this way, we obtain a scheduler that realises a conservative two-phase locking protocol for persistent programming language transactions. We apply the analysis to a language that is a significant subset of Galileo. The goal of the analysis is to detect the accesses solely to shareable and modifiable persistent data.