Skip to content

Commit

Permalink
Tap
Browse files Browse the repository at this point in the history
  • Loading branch information
@imbrem
imbrem committed Oct 6, 2024
1 parent 40f1cc4 commit b06b630
Show file tree
Hide file tree
Showing 2 changed files with 206 additions and 22 deletions.
95 changes: 83 additions & 12 deletions paper.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3734,18 +3734,9 @@ \subsection{TSO weak memory}

\section{Discussion and Related Work}

\TODO{Release-acquire lore; event structure lore}
\subsection{Linearity, Guardedness, and Friends}

\TODO{Ye Olde Related Work List:}
\begin{itemize}
\item \citet{liang-95-interpreters} to build interpreters supporting effects using monad stacks
\item Alternative pomset lore:
\begin{itemize}
\item \citet{jagadeesan-pwp-20}
\item \citet{leaky-semicolon}
\end{itemize}
\item Release/acquire lore from \citet{release-acquire}
\item Event structures lore: ask Neel
\item \citet{fuhrmann-direct-1999} for:
\begin{itemize}
\item Linearity (relevant -- copyability, affine -- discardability)
Expand All @@ -3755,8 +3746,88 @@ \section{Discussion and Related Work}
Elgot structure?
\item See also: \citet{Thielecke1997CategoricalSO}
\end{itemize}
\item Monadic models of syntax: \citet{ullrich-22-do-unchained}
\item Rewriting in the presence of weak memory: \citet{sevcik-drf-sc}
\item \citet{coinductive-resumption-levy-goncharov-19} introduce guarded Elgot categories +
monads, which allow us to reason about guarded iteration:
\begin{itemize}
\item Identity is the initial guarded Elgot monad, admits only acyclic CFGs, this is interesting
as these are equivalent to expressions
\item Can reason about e.g. productivity, terminating programs, etc. under the \isotopessa{}
framework this way
\item The coinductive resumption monad defined in this paper might be useful for reasoning about
potentially nonterminating processes in \isotopessa{} models, somehow...
\end{itemize}
\end{itemize}

\subsection{General Models}


\begin{itemize}
\item \citet{liang-95-interpreters} to build interpreters supporting effects using monad stacks;
because Elgot monads become \isotopessa{} models and many monad transformers preserve Elgot
structure, this can let us build up many useful models.
\end{itemize}


\subsection{Compositional Relaxed Memory Concurrency}

\begin{itemize}
\item \citet{batty-compositional-17} is a survey which describes why one would want to use
denotational semantics for relaxed memory concurrency, and some basic compositionality properties
\item \citet{jagadeesan-pwp-20} is an attempt to build a denotational model with pomsets, pomsets
with preconditions, but semicolon is \emph{not} associative, \citet{leaky-semicolon} works on this
to get pomsets with predicate transformers, and makes things associative, which is an important
feature for reasoning about composition since it lets us do category theory. However, it does not
yet support loops.
\item \citet{brookes-full-abstraction-96} uses traces to model SC; pretty sure you can get a monad
out of this
\item There is a \citet{brookes-full-abstraction-96}-style semantics for x86 TSO in
\citet{jagadeesan-brookes-relaxed-12}; does this give an alternative monad? How does it compare to
\citet{sparky}?
\item Release/acquire lore from \citet{release-acquire}: already a monad, but would need to show
it's Elgot to get an \isotopessa{} model
\item \citet{paviotti-modular-relaxed-dep-20} uses event structures to build a denotational
semantics for relaxed memory concurrency, compositionality is via the ``hole''
method.
\item Something about step indexing...
\end{itemize}

\subsection{Other SSA type systems}

\begin{itemize}
\item \citet{typed-effect-ssa-rigon-torrens-vasconcellos-20} give a typed translation
from SSA into the lambda calculus, into a type-and-effect system.
\item \citet{ssa-types-matsuno-ohori-06} give a type theory for what appear to be
ordinary three-address code programs. However, every well-typed program can be
placed into SSA-form by inserting $\phi$-nodes in a fully type-directed way.
This lets them model SSA without any $\phi$-nodes, lets them use the standard
semantics for three-address code.
\item \citet{hua-explicit-ssa-2010} give another type system and direct operational
semantics for SSA, and proves type safety for it.
\item Many operational semantics for SSA have arisen from compiler verification
efforts. \citet{barthe-compcert-ssa-2014} give an operational semantics as part
of the CompCertSSA project, and give a semantics-preserving translation from
three-address code into SSA. \citet{herklotz-gsa-2023} formalise "gated SSA" and
give semantics-preserving translations between it and ordinary SSA. Going beyond
CompCertSSA, \citet{vellum} have studied the semantics of the LLVM IR itself.
\item
There has been much less work on denotational semantics for SSA, or directly on
its equational theory. \citet{pop-ssa-inout-2009} give an unusual denotational
model of SSA in terms of the iteration structure of a program, which they use to
better understand the loop-closing $\phi$-nodes found both in the gated SSA
representation as well as practical compilers such as GCC.
\citet{garbuzov-structural-cfg-2018} exhibit a correspondence between an
operational semantics for SSA, and an operational semantics for
call-by-push-value~\cite{cbpv}. They use the normal-form bisimulations of
\citet{lassen-bisim} to derive an equational theory for use in justifying
optimisations. Their operational semantics is effect-free, which means that it
cannot justify optimisations such as eliminating redundant writes.
\end{itemize}

\subsection{MLIR lore}

\begin{itemize}
\item \citet{siddharth-24-peephole} for verifying peephole optimisations in SSA, also formalized
in Lean 4, in the context of MLIR
\end{itemize}

\bibliographystyle{ACM-Reference-Format}
Expand Down
133 changes: 123 additions & 10 deletions references.bib
View file
Original file line number Diff line number Diff line change
Expand Up @@ -477,16 +477,22 @@ @article{rvsdg
keywords = {LLVM, intermediate representation, Regionalized value state dependence graph (RVSDG)}
}

%TODO: fix this with a proper citation
@misc{carette-central-2022,
title = {Central Submonads and Notions of Computation: Soundness, Completeness
and Internal Languages},
author = {Titouan Carette and Louis Lemonnier},
year = {2022},
month = {6},
eprint = {2207.09190},
archiveprefix = {arXiv},
primaryclass = {Logic in Computer Science}
@inproceedings{carette-central-2022,
author = {Titouan Carette and
Louis Lemonnier and
Vladimir Zamdzhiev},
title = {Central Submonads and Notions of Computation: Soundness, Completeness
and Internal Languages},
booktitle = {38th Annual {ACM/IEEE} Symposium on Logic in Computer Science, {LICS}
2023, Boston, MA, USA, June 26-29, 2023},
pages = {1--13},
publisher = {{IEEE}},
year = {2023},
url = {https://doi.org/10.1109/LICS56636.2023.10175687},
doi = {10.1109/LICS56636.2023.10175687},
timestamp = {Wed, 29 May 2024 16:05:22 +0200},
biburl = {https://dblp.org/rec/conf/lics/CaretteLZ23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{fuhrmann-direct-1999,
Expand Down Expand Up @@ -953,4 +959,111 @@ @article{bohm-jacopini
month = may,
pages = {366–371},
numpages = {6}
}

@article{batty-compositional-17,
author = {Batty, Mark },
title = {Compositional relaxed concurrency},
journal = {Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences},
volume = {375},
number = {2104},
pages = {20150406},
year = {2017},
doi = {10.1098/rsta.2015.0406},
URL = {https://royalsocietypublishing.org/doi/abs/10.1098/rsta.2015.0406},
eprint = {https://royalsocietypublishing.org/doi/pdf/10.1098/rsta.2015.0406}
}

@article{brookes-full-abstraction-96,
author = {Stephen D. Brookes},
title = {Full Abstraction for a Shared-Variable Parallel Language},
journal = {Inf. Comput.},
volume = {127},
number = {2},
pages = {145--163},
year = {1996},
url = {https://doi.org/10.1006/inco.1996.0056},
doi = {10.1006/INCO.1996.0056},
timestamp = {Fri, 12 Feb 2021 22:16:48 +0100},
biburl = {https://dblp.org/rec/journals/iandc/Brookes96.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{jagadeesan-brookes-relaxed-12,
author = {Radha Jagadeesan and
Gustavo Petri and
James Riely},
editor = {Lars Birkedal},
title = {Brookes Is Relaxed, Almost!},
booktitle = {Foundations of Software Science and Computational Structures - 15th
International Conference, {FOSSACS} 2012, Held as Part of the European
Joint Conferences on Theory and Practice of Software, {ETAPS} 2012,
Tallinn, Estonia, March 24 - April 1, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7213},
pages = {180--194},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-28729-9\_12},
doi = {10.1007/978-3-642-28729-9\_12},
timestamp = {Tue, 14 May 2019 10:00:55 +0200},
biburl = {https://dblp.org/rec/conf/fossacs/JagadeesanPR12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{coinductive-resumption-levy-goncharov-19,
author = {Paul Blain Levy and
Sergey Goncharov},
editor = {Markus Roggenbach and
Ana Sokolova},
title = {Coinductive Resumption Monads: Guarded Iterative and Guarded Elgot},
booktitle = {8th Conference on Algebra and Coalgebra in Computer Science, {CALCO}
2019, June 3-6, 2019, London, United Kingdom},
series = {LIPIcs},
volume = {139},
pages = {13:1--13:17},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2019},
url = {https://doi.org/10.4230/LIPIcs.CALCO.2019.13},
doi = {10.4230/LIPICS.CALCO.2019.13},
timestamp = {Wed, 21 Aug 2024 22:46:00 +0200},
biburl = {https://dblp.org/rec/conf/calco/Levy019.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{mlir-effect-handlers-yu-23,
author = {Yu, Pingshi},
title = {Reasoning about MLIR Semantics through Effects and Handlers},
year = {2023},
isbn = {9798400702211},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3597926.3605239},
doi = {10.1145/3597926.3605239},
abstract = {MLIR is a novel framework for developing intermediate representations (IRs) of compilers. At its core, MLIR is a framework for the specification of syntax fragments (dialects) and optimisations, which can be combined \`{a}−la−carte to form customised IRs. Through this, MLIR allows IR abstractions to be shared across different domains. With rapid adoption of MLIR across industry, techniques for formalised semantics which matches the flexibility and extensibility offered by MLIR are urgently needed. We propose a framework for MLIR semantics based on effect handlers, which allows for dialect semantics to be specified in a modular and composable way, parallel to MLIR. We also describe several research directions continuing on from handlers-based MLIR semantics.},
booktitle = {Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis},
pages = {1552–1554},
numpages = {3},
keywords = {interpreters, algebraic effects, Semantics, MLIR},
location = {Seattle, WA, USA},
series = {ISSTA 2023}
}

@InProceedings{siddharth-24-peephole,
author = {Bhat, Siddharth and Keizer, Alex and Hughes, Chris and Goens, Andr\'{e}s and Grosser, Tobias},
title = {{Verifying Peephole Rewriting in SSA Compiler IRs}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {9:1--9:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.9},
URN = {urn:nbn:de:0030-drops-207372},
doi = {10.4230/LIPIcs.ITP.2024.9},
annote = {Keywords: compilers, semantics, mechanization, MLIR, SSA, regions, peephole rewrites}
}

0 comments on commit b06b630

Please sign in to comment.