From 8cc769f4af85fdcc71b96116633e67045d71c6f0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jasper=20Gr=C3=A4flich?= <graeflich@uni-potsdam.de>
Date: Wed, 27 Sep 2023 15:57:43 +0200
Subject: [PATCH] Clean up unused section "use-based references"
---
use-based-refs/use-based-refs.pdf | 4 +--
use-based-refs/use-based-refs.tex | 57 -------------------------------
2 files changed, 2 insertions(+), 59 deletions(-)
diff --git a/use-based-refs/use-based-refs.pdf b/use-based-refs/use-based-refs.pdf
index db25cf6..fa12378 100644
--- a/use-based-refs/use-based-refs.pdf
+++ b/use-based-refs/use-based-refs.pdf
@@ -1,3 +1,3 @@
version https://git-lfs.github.com/spec/v1
-oid sha256:b46647f538ab1fd4a27ed5bf54da16d1c191a901cf8395a838a0f88a4b2ccf8e
-size 199524
+oid sha256:d820c6621f77b3474c0ec8e3b52c386d001e735e302f6248cc282a156acd414d
+size 194723
diff --git a/use-based-refs/use-based-refs.tex b/use-based-refs/use-based-refs.tex
index 81e2cff..ed14726 100644
--- a/use-based-refs/use-based-refs.tex
+++ b/use-based-refs/use-based-refs.tex
@@ -78,63 +78,6 @@ We propose an alternative approach to borrow checking by introducing
\item a formalization of these concepts in an extension to a simple $\lambda$-calculus (\autoref{sec:formalization}).
\end{itemize}
-\section{Location and Provenance}\label{sec:use-based-refs}
-
-To enforce AXM, there are three pieces of information that must be known at each point during execution:
-
-\begin{itemize}
- \item All references which may be accessed at that point,
- \item The kind of access, that is read or write, and
- \item which of these references may alias.
-\end{itemize}
-
-It can then be guaranteed that no set of references violates AXM. To ensure this, a reference comes with the following data:
-
-\begin{itemize}
- \item A unique identifier which is generated at the point of creation of the reference.\todo[inline]{Do we allow creation of references outside of variable definitions? Otherwise, we could have reference id = variable name, assuming single static assignment.}
- \item A \emph{provenance}, that is a set of locations that the reference may point to. Two references may alias if they have overlapping provenance.
-\end{itemize}
-
-\subsection{Concrete Locations}
-
-Locations can be \emph{concrete} or \emph{abstract}. A \emph{concrete location} is created by an allocation and refers to the portion of memory which is reserved by the allocation. For example, in the code
-
-\begin{algorithmic}
- \State{$r_1$ \gets \Call{alloc}{$T$}}
- \State{$r_2$ \gets $\&v$}
-\end{algorithmic}
-
-$r_1$ is the result of an allocation, meaning there is a concrete location $l$ and the provenance of $r_1$ is just the set $\{l\}$. Further, $r_2$ is derived from $r_1$ and inherits its provenance.
-
-\subsection{Abstract Locations}
-
-An \emph{abstract location} is used as a standin whenever the concrete location is not known because it is e.g. passed as a function argument. For example, in
-
-\begin{algorithmic}
- \Function{TakeTwo}{$r_1 \colon \&T$, $r_2 \colon \&T$}
- \State{$e$}
- \EndFunction
-\end{algorithmic}
-
-the concrete locations are not known, necessitating us to create a fresh abstract location $p_i$ for each $r_i$. Since $r_1$ and $r_2$ are of the same type, they may alias, for example through a call like the following:
-
-\begin{algorithmic}
- \State{$r$ \gets \Call{alloc}{$T$}}
- \State{\Call{TakeTwo}{$r$, $r$}}
-\end{algorithmic}
-
-Thus both references have the same provenance $\{p_1, p_2\}$.
-
-% Additionally, we need a \emph{state graph}. It augments the control-flow graph of the program by keeping track for each node of all references that are in scope at that point. References may be in several \emph{states}:
-
-% \begin{itemize}
-% \item An \emph{inactive} reference is guaranteed to not be used at this point,
-% \item a reference in the \emph{read} state may be read but not be written to,
-% \item the \emph{write} allows writing as well as reading, and
-% \item a \emph{dead} reference may not be accessed until it falls of scope.
-% \item {\color{red} \emph{drop/own} can be dropped, for owning pointers?}
-% \end{itemize}
-
\section{Regions and Aliasing}\label{sec:provenance}
We propose that the construction of provenance sets shall only rely on the local context of a function $f$. There are three ways of bringing a reference into context, each of which comes with a different way to determine its region.
--
GitLab