{"id":{"repo_id":"cambridge","oai_identifier":"oai:www.repository.cam.ac.uk:1810/354249"},"canonical_url":"https://search.dev.ndltd.org/etd/cambridge/oai:www.repository.cam.ac.uk:1810/354249","repository":{"repo_id":"cambridge","name":"Cambridge University","base_url":"https://api.repository.cam.ac.uk/server/oai/request"},"display":{"title":"Furthering Datalog in the pursuit of program analysis","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Isaacs, Joseph"],"institution":"University of Cambridge","degree_name":"Doctor of Philosophy (PhD)","degree_level":"Doctoral","degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":["Jones, Timothy","Mycroft, Alan"],"committee_chairs":[],"committee_members":[],"year":2022,"date_issued":"2022-07-22","date_published":"2022-07-22","updated_at":"2026-07-22T22:24:21Z","subjects":["computer science"],"languages":["eng"],"rights":[],"rights_urls":["https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/0552a9e4-156d-4e96-a8ab-73ab9e2ab582/download","https://creativecommons.org/licenses/by-sa/4.0/"],"identifier_entries":[]},"links":{"outbound_url":"https://doi.org/10.17863/CAM.100114","outbound_label":"DOI","outbound_source":"dc:identifier.doi"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Jones, Timothy","Mycroft, Alan"]},{"key":"dc:contributor.sponsor","label":"Sponsor","values":["EPSRC iCASE studentship in conjunction with Arm"]},{"key":"dc:creator","label":"Author","values":["Isaacs, Joseph"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.issued","label":"Date","values":["2022-07-22"]},{"key":"dc:publisher.institution","label":"Dc Publisher Institution","values":["University of Cambridge"]},{"key":"dc:relation.isreferencedby.uri","label":"Dc Relation Isreferencedby URI","values":["https://www.repository.cam.ac.uk/handle/1810/354249"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"dc:type.qualificationlevel","label":"Dc Type Qualificationlevel","values":["Doctoral"]},{"key":"dc:type.qualificationname","label":"Dc Type Qualificationname","values":["Doctor of Philosophy (PhD)"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["computer science"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/0552a9e4-156d-4e96-a8ab-73ab9e2ab582/download","https://creativecommons.org/licenses/by-sa/4.0/"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.doi","label":"DOI","values":["https://doi.org/10.17863/CAM.100114"]},{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/6ef091ab-d041-4baa-93d3-f6c9bbb16f94/download"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:format.checksum.md5","label":"Dc Format Checksum Md5","values":["31e18b63d4fcc0ba626b03850449afa0","87eda9de84448d1f82354d60eee3eb5f"]},{"key":"dc:title","label":"Title","values":["Furthering Datalog in the pursuit of program analysis"]}]}],"canonical_facts":{"dc:contributor.advisor":["Jones, Timothy","Mycroft, Alan"],"dc:contributor.sponsor":["EPSRC iCASE studentship in conjunction with Arm"],"dc:creator":["Isaacs, Joseph"],"dc:date.issued":["2022-07-22"],"dc:description.abstract":["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."],"dc:format.checksum.md5":["31e18b63d4fcc0ba626b03850449afa0","87eda9de84448d1f82354d60eee3eb5f"],"dc:identifier.doi":["https://doi.org/10.17863/CAM.100114"],"dc:identifier.uri":["https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/6ef091ab-d041-4baa-93d3-f6c9bbb16f94/download"],"dc:language":["eng"],"dc:publisher.institution":["University of Cambridge"],"dc:relation.isreferencedby.uri":["https://www.repository.cam.ac.uk/handle/1810/354249"],"dc:rights":["https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/0552a9e4-156d-4e96-a8ab-73ab9e2ab582/download","https://creativecommons.org/licenses/by-sa/4.0/"],"dc:subject":["computer science"],"dc:title":["Furthering Datalog in the pursuit of program analysis"],"dc:type":["Thesis"],"dc:type.qualificationlevel":["Doctoral"],"dc:type.qualificationname":["Doctor of Philosophy (PhD)"]},"updated_at":"2026-07-22T22:24:21Z"}