related and citations for PL material

main
Kristopher Micinski 2023-07-18 01:20:53 -04:00
parent 68cee7c1ff
commit 91ee62f7d4
2 changed files with 71 additions and 1 deletions

View File

@ -1,3 +1,22 @@
@inproceedings{Bravenboer:2009,
author = {Bravenboer, Martin and Smaragdakis, Yannis},
title = {Strictly Declarative Specification of Sophisticated Points-to Analyses},
year = {2009},
isbn = {9781605587660},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/1640089.1640108},
doi = {10.1145/1640089.1640108},
abstract = {We present the DOOP framework for points-to analysis of Java programs. DOOP builds on the idea of specifying pointer analysis algorithms declaratively, using Datalog: a logic-based language for defining (recursive) relations. We carry the declarative approach further than past work by describing the full end-to-end analysis in Datalog and optimizing aggressively using a novel technique specifically targeting highly recursive Datalog programs.As a result, DOOP achieves several benefits, including full order-of-magnitude improvements in runtime. We compare DOOP with Lhotak and Hendren's PADDLE, which defines the state of the art for context-sensitive analyses. For the exact same logical points-to definitions (and, consequently, identical precision) DOOP is more than 15x faster than PADDLE for a 1-call-site sensitive analysis of the DaCapo benchmarks, with lower but still substantial speedups for other important analyses. Additionally, DOOP scales to very precise analyses that are impossible with PADDLE and Whaley et al.'s bddbddb, directly addressing open problems in past literature. Finally, our implementation is modular and can be easily configured to analyses with a wide range of characteristics, largely due to its declarativeness.},
booktitle = {Proceedings of the 24th ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications},
pages = {243262},
numpages = {20},
keywords = {bdds, datalog, declarative, points-to analysis, DOOP},
location = {Orlando, Florida, USA},
series = {OOPSLA '09}
}
@article{Cocke:1977,
author = {Cocke, John and Kennedy, Ken},
title = {An Algorithm for Reduction of Operator Strength},
@ -18,6 +37,43 @@ numpages = {7},
keywords = {operator strength reduction, optimization of compiled code, compilers, program analysis, test replacement, strongly connected region}
}
@inproceedings{doop-souffle,
author = {Antoniadis, Tony and Triantafyllou, Konstantinos and Smaragdakis, Yannis},
title = {Porting Doop to Souffl\'{e}: A Tale of Inter-Engine Portability for Datalog-Based Analyses},
year = {2017},
isbn = {9781450350723},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3088515.3088522},
doi = {10.1145/3088515.3088522},
abstract = {We detail our experience of porting the static analysis framework to the recently introduced Datalog engine. The port addresses the idiosynchrasies of the Datalog dialects involved (w.r.t. the type system, value construction, and fact updates) and differences in the runtime systems (w.r.t. parallelism, transactional execution, and optimization methodologies). The overall porting effort is interesting in many ways: as an instance of the benefits of specifying static analyses declaratively, gaining benefits (e.g., parallelism) from a mere porting to a new runtime system; as a study of the effort required to migrate a substantial Datalog codebase (of several thousand rules) to a different dialect. By exploiting shared-memory parallelism, the version of the framework achieves speedups of up to 4x, over already high single-threaded performance.},
booktitle = {Proceedings of the 6th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis},
pages = {2530},
numpages = {6},
keywords = {Datalog, Points-to analysis, Doop},
location = {Barcelona, Spain},
series = {SOAP 2017}
}
@article{egglog,
author = {Zhang, Yihong and Wang, Yisu Remy and Flatt, Oliver and Cao, David and Zucker, Philip and Rosenthal, Eli and Tatlock, Zachary and Willsey, Max},
title = {Better Together: Unifying Datalog and Equality Saturation},
year = {2023},
issue_date = {June 2023},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {7},
number = {PLDI},
url = {https://doi.org/10.1145/3591239},
doi = {10.1145/3591239},
abstract = {We present egglog, a fixpoint reasoning system that unifies Datalog and equality saturation (EqSat). Like Datalog, egglog supports efficient incremental execution, cooperating analyses, and lattice-based reasoning. Like EqSat, egglog supports term rewriting, efficient congruence closure, and extraction of optimized terms. We identify two recent applications -- a unification-based pointer analysis in Datalog and an EqSat-based floating-point term rewriter -- that have been hampered by features missing from Datalog but found in EqSat or vice-versa. We evaluate our system by reimplementing those projects in egglog. The resulting systems in egglog are faster, simpler, and fix bugs found in the original systems.},
journal = {Proc. ACM Program. Lang.},
month = {jun},
articleno = {125},
numpages = {25},
keywords = {Rewrite systems, Program optimization, Equality saturation, Datalog}
}
@inproceedings{Tate:2009,
author = {Tate, Ross and Stepp, Michael and Tatlock, Zachary and Lerner, Sorin},

View File

@ -1,8 +1,22 @@
\section{Related Work}
Database-inspired optimizations (semi-na\"ive evaluation and indexing)
have been the enabling force behind recent orders-of-magnitude
scalability gains in context-sensitive points to
analysis~\cite{Bravenboer:2009}. In particular, the Datalog engine
Souffl\'e has proven a de-facto target for the implementation of
high-performance reachability-based analyses~\cite{doop-souffle}. Our
work is primarily distinguished by its focus on \emph{structural}
constraints, which are largely ignored by these engines and (in our
experience) result in significant performance losses in workloads
which manipulate structured data. Our notion of optimization is more
closely related to equality saturation, which applies rewrite rules to
a fixed-point~\cite{Tate:2009}. Recent work in this area leverages
compressed representations, namely union-find~\cite{egglog}.
\begin{itemize}
\item Kristopher's papers
\item DBToaster/etc...
\item TreeToaster / Fluid Data Structures
\item Graph/Tree databases (work on XML/Json querying?)
\end{itemize}
\end{itemize}