2026-09-20T05:00:33Zhttps://api.repository.cam.ac.uk/server/oai/request

oai:www.repository.cam.ac.uk:1810/3542492024-12-28T01:47:45Zcom_1810_219481com_1810_256065col_1810_219482

Furthering Datalog in the pursuit of program analysis https://doi.org/10.17863/CAM.100114 Isaacs, Joseph Jones, Timothy Mycroft, Alan This thesis focuses on specifying compiler analyses in a declarative language, namely Datalog. This work contains three contributions: expanding the number of programs Datalog, specifically Soufflé (a superset of Datalog), can support; providing a declarative implementation of a well-known analysis; and introducing a new program analysis. First, a new construct is introduced into Soufflé allowing consistent negation of relations used to infer facts about that same negated relation. This can be seen as a join point in inference when a rule partially pauses inference until the negated relation is in a consistent state, and it is safe to evaluate the negation. Soufflé, with consistent negation, is then used to specify a natural encoding of a depth-first graph exploration using a visited set and the sum of affine multivariable polynomials with partially disjoint variable domains. The technique allows previously difficult-to-implement problems to be implemented with asymptotically better performance, in a more natural and expressive fashion. Second, a declarative implementation of GVN is presented—a common program analysis to find equivalent program variables—called DGVN. This implementation breaks a data dependence throughout the whole GVN algorithm that previously limited its parallelism. The Soufflé implementation also makes use of the previously described new negation-aiding construct to increase performance and to allow a natural expression of the algorithm. DGVN is complete enough to be evaluated on benchmarks from Specint. Third, a definition of pairwise program commutativity is presented, useful to automatic parallelising compilers that transform data dependency graphs. This definition is then lifted into the set domain, allowing for interface-boundary respecting commutativity specifications using semantic program properties, as source-code inline annotations. This system is then used to encode commutative functions from libc and other common data structures and employed to parallelise several benchmark applications. University of Cambridge 2022-07-22 Thesis Doctoral Doctor of Philosophy (PhD) eng EPSRC iCASE studentship in conjunction with Arm https://www.repository.cam.ac.uk/handle/1810/354249 https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/6ef091ab-d041-4baa-93d3-f6c9bbb16f94/download 31e18b63d4fcc0ba626b03850449afa0 https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/0552a9e4-156d-4e96-a8ab-73ab9e2ab582/download 87eda9de84448d1f82354d60eee3eb5f https://creativecommons.org/licenses/by-sa/4.0/ computer science