Data sharing analysis for a database programming language via abstract interpretation

This paper presents an experiment of 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 detecting opportunities of safe parallelism for transaction operations scheduling. Transaction operations can be safely interleaved when there is no overlapping among their readsets and writesets. A non-standard interpreter performs the analysis. Such an interpreter, given the text of the 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 are provided to the scheduler before beginning the execution of transaction operations. In this way, we obtain a scheduler that implements 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. It is worth noting that the goal of the analysis is to count the accesses solely to shareable and modifiable persistent data structures.