Index: /Deliverables/D6.3/report.tex
===================================================================
--- /Deliverables/D6.3/report.tex (revision 3122)
+++ /Deliverables/D6.3/report.tex (revision 3123)
@@ -456,5 +456,5 @@
statistical informations on the last executions of the branch.
-\paragraph{The labelling appraoch for data independent cost models}
+\paragraph{The labelling approach for data independent cost models}
We now describe how the labelling approach can be slightly modified to deal
with a data independent cost model $(\hookrightarrow,K)$ built over
@@ -602,5 +602,5 @@
\begin{figure}[t]
-\begin{center}
+\begin{tiny}
\begin{verbatim}
int fact (int n) {
@@ -614,5 +614,5 @@
}
\end{verbatim}
-\end{center}
+\end{tiny}
\caption{A simple program that computes the factorial of 10.\label{factprog}}
\end{figure}
@@ -730,3 +730,161 @@
\end{itemize}
+\paragraph{The problem with caches}
+Cost models for pipelines --- at least simple ones --- are data independent,
+i.e. they are dependent on a view that is execution path dependent. In other
+words, the knowledge about the sequence of executed instructions is sufficient
+to predict the cost of future instructions.
+
+The same property does not hold for caches. The cost of accessing a memory
+cell strongly depends on the addresses of the memory cells that have been read
+in the past. In turn, the accessed addresses are a function of the low level
+data state, that cannot be correlated to the source program state.
+
+The strong correlation between the internal state of caches and the data
+accessed in the past is one of the two main responsibles for the lack of
+precision of static analysis in modern uni-core architectures. The other one
+is the lack of precise knowledge on the real behaviour of modern hardware
+systems. In order to overcome both problems, that Cazorla\&alt.~\cite{proartis}
+call the ``\emph{Timing Analysis Walls}'', the PROARTIS European Project has
+proposed to design ``\emph{a hardware/software architecture whose execution
+timing behaviour eradicates dependence on execution history}'' (\cite{proartis}, Section 1.2). The statement is obviously too strong. What is concretely
+proposed by PROARTIS is the design of a hardware/software architecture whose
+execution timing is \emph{execution path dependent} (our terminology).
+
+We have already seen that we are able to accomodate in the labelling approach
+cost functions that are dependent on views that are execution path dependent.
+Before fully embracing the PROARTIS vision,
+we need to check if there are other aspects of the PROARTIS proposal
+that can be problematic for CerCo.
+
+\paragraph{Static Probabilistic Time Analysis}
+The approach of PROARTIS to achieve execution path dependent cost models
+consists in turning the hard-to-analyze deterministic hardware components
+(e.g. the cache) into probabilistic hardware components. Intuitively,
+algorithms that took decision based on the program history now throw a dice.
+The typical example which has been thoroughly studied in
+PROARTIS~\cite{proartis2} is that of caches. There the proposal is to replace
+the commonly used deterministic placement and replacement algorithms (e.g. LRU)
+with fully probabilistic choices: when the cache needs to evict a page, the
+page to be evicted is randomly selected according to the uniform distribution.
+
+The expectation is that probabilistic hardware will have worse performances
+in the average case, but it will exhibit the worst case performance only with
+negligible probability. Therefore, it becomes no longer interesting to estimate
+the actual worst case bound. What becomes interesting is to plot the probability
+that the execution time will exceed a certain treshold. For all practical
+purposes, a program that misses its deadline with a negligible probability
+(e.g. $10^-9$ per hour of operation) will be perfectly acceptable when deployed
+on an hardware system (e.g. a car or an airplane) that is already specified in
+such a way.
+
+In order to plot the probability distribution of execution times, PROARTIS
+proposes two methodologies: Static Probabilistic Time Analysis (SPTA) and
+Measurement Based Probabilistic Time Analysis (MBPTA). The first one is
+similar to traditional static analysis, but it operates on probabilistic
+hardware. It is the one that we would like to embrace. The second one is
+based on measurements and it is justified by the following assumption: if
+the probabilities associated to every hardware operation are all independent
+and identically distributed, then measuring the fime spent on full runs of
+sub-systems components yields a probabilistic estimate that remains valid
+when the sub-system is plugged in a larger one. Moreover, the probabilistic
+distribution of past runs must be equal to the one of future runs.
+
+We understand that MBPTA is useful to analyze closed (sub)-systems whose
+functional behavior is deterministic. It does not seem to have immediate
+applications to parametric time analysis, which we are interested in.
+Therefore we focus on SPTA.
+
+According to~\cite{proartis},
+``\emph{in SPTA, execution time probability distributions for individual operations \ldots are determined statically
+from a model of the processor. The design principles of PROARTIS
+will ensure \ldots that the probabilities for the execution time of each
+instruction are independent. \ldots SPTA is performed by calculating the
+convolution ($\oplus$) of the discrete probability distributions which describe
+the execution time for each instruction on a CPU; this provides a probability
+distribution \ldots representing the timing behaviour of the entire sequence of
+instructions.}''
+
+We will now analyze to what extend we can embrace SPTA in CerCo.
+
+\paragraph{The labelling approach for Static Probabilistic Time Analysis}
+
+To summarize, the main practical differences between standard static time
+analysis and SPTA are:
+\begin{itemize}
+ \item The cost functions for single instructions or sequences of instructions
+ no longer return a natural numbers (number of cost units) but integral
+ random variables.
+ \item Cost functions are extended from single instructions to sequences of
+ instructions by using the associative convolution operator $\oplus$
+\end{itemize}
+
+By reviewing the papers that described the labelling approach, it is easy to
+get convinced that the codomain of the cost analysis can be lifted from
+that of natural numbers to any group. Moreover, by imposing labels after
+every function call, commutativity can be dropped and the approach works on
+every monoid (usually called \emph{cost monoids} in the litterature).
+Because random variables and convolutions form a monoid, we immediately have
+that the labelling approach extends itself to SPTA. The instrumented code
+produced by an SPTA-CerCo compiler will then have random variables (on a finite
+domain) as costs and convolutions in place of the \texttt\{\_\_cost\_incr\}
+function.
+
+What is left to be understood is the way to state and compute the
+probabilistic invariants to do \emph{parametric SPTA}. Indeed, it seems that
+PROARTIS only got interested into non parametric PTA. For example, it is
+well known that actually computing the convolutions results in an exponential
+growth of the memory required to represent the result of the convolutions.
+Therefore, the analysis should work symbolically until the moment where
+we are interested into extracting information from the convolution.
+
+Moreover, assuming that the problem of computing invariants is solved,
+the actual behavior of automated theorem
+provers on probabilistic invariants is to be understood. It is likely that
+a good amount of domain specific knowledge about probability theory must be
+exploited and incorporated into automatic provers to achieve concrete results.
+
+Parametric SPTA using the methodology developed in CerCo is a future research
+direction that we believe to be worth exploring in the middle and long term.
+
+\paragraph{Static Probabilistic Time Analysis for Caches in CerCo}
+
+As a final remark, we note that the analysis in CerCo of systems that implement
+probabilistic caches requires a combination of SPTA and data independent cost
+models. The need for a probabilistic analysis is obvious but, as we saw in
+the previous paragraph, it requires no modification of the labelling approach.
+
+In order to understand the need for dependent labelling (to work on data
+independent cost functions), we need to review the behaviour of probabilistic
+caches as proposed by PROARTIS. The interested reader can
+consult~\cite{proartis2-articolo30} for further informations.
+
+In a randomized cache, the probability of evicting a given line on every access
+is $1/N$ where $N$ stands for the number of cache entries. Therefore the
+hit probability of a specific access to such a cache is
+$P(hit) = (\frac{N-1}{N})^K$ where $K$ is the number of cache misses between
+two consecutive accesses to the same cache entry. For the purposes of our
+analysis, we must assume that every cache access could cause an eviction.
+Therefore, we define $K$ (the \emph{reuse distance}) to be the number of
+memory accesses between two consecutive accesses to the same cache entry,
+including the access for which we are computing $K$. In order to compute
+$K$ for every code memory address, we need to know the execution path (in
+our terminology). In other words, we need a view that records for each
+cache entry the number of memory accesses that has occurred since the last
+access.
+
+For pipelines with $n$ stages, the number of possible views is limited to
+$2^n$: a view can usually just be represented by a word. This is not the
+case for the views on caches, which are in principle very large. Therefore,
+the dependent labelling approach for data indepedent cost functions that we
+have presented here could still be unpractical for caches. If that turns out
+to be the case, a possible strategy is the use of abstract interpretations
+techniques on the object code to reduce the size of views exposed at the
+source level, at the price of an early loss of precision in the analysis.
+
+More research work must be performed at the current stage to understand if
+caches can be analyzed, even probabilistically, using the CerCo technology.
+This is left for future work and it will be postponed after the work on
+pipelines.
+
\end{document}