% Author: Olaf Chitil
% Created: 25.3.2002
% Last Update: 
  
\documentclass[12pt]{article}
\usepackage[a4paper]{geometry}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{alltt}
\usepackage{url}


%------------------------------------------------------------------------------

\begin{document}
\thispagestyle{empty}

\title{ART Memo 34 (Version 0)\\The Challenge of Transforming Trusted Code} 
\author{Olaf Chitil}
\date{\today}
\maketitle

%------------------------------------------------------------------------------

\section{Introduction}

Hat 2.00 transforms both traced and untraced, that is trusted, code. The transformation itself is --- ignoring some minor optimisations --- the same for both, except that untraced transformed code uses a different set of combinators of the Hat library.

Calling untransformed functions from transformed code is currently limited to non-overloaded functions, because we do not know how a wrapper could unwrap a class dictionary. Furthermore, the history of the result of the call is lost in so far that the whole result structure is attributed to this call of an untransformed function, although the function may actually pass back parts of its arguments. 

\section{What to Record in the Trace}

The computation of trusted code is not traced, but the combinators have to record in the trace for each traced application of a trusted function its call, the computations of any traced functions called by it (the trusted function may be higher-order or even call traced code explicitly), and its result.

Recording the call and all traced subcomputations is quite straightforward, because a trusted redex always passes its right-hand-side a Hidden node as parent. So by testing if a parent is a Hidden node both trusted and traced code can determine if they are called from trusted code.

The problem is recording the result. Note that the result value of a trusted function may contain functions. Such a function is currently only recorded as trusted expression \texttt{\{?\}}. The alternative would be to show arbitrary large subexpressions of trusted code, which does not seem to be desirable because trusting sets an abstraction barrier and it would also be hard to implement. So only non-functional result values are recorded at all.

\section{Record all Values}

In our first implementation of trusting, combinators did not record any reductions in trusted code, but all constructions of values. The disadvantage of this implementation is that not only the result value of a trusted function but also all intermediate data structures of the trusted computation are recorded.

\section{Demand-Driven Recording}

Our current implementation takes advantage of lazy evaluation to only record those values constructed in trusted code that are \emph{demanded} from traced code. Thus no superfluous values are recorded.

The problem with this implementation is in the definition of the function application combinators \texttt{uap}\emph{i}, more precisely in the helper function \texttt{uwrapForward}:

\begin{alltt}
uap1 :: RefSrcPos -> RefExp -> R (Fun a z) -> R a -> R z
uap1 sr h (R (Fun f) _) a = uwrapForward h (f h a)

uwrapForward :: RefExp -> R a -> R a
uwrapForward h x =
  let status = unsafePerformIO (newIORef (Hidden h))
  in status `seq`
     R (case unsafePerformIO (readIORef status) of
          Hidden _ -> 
            case x of 
              R rv tv -> unsafePerformIO (writeIORef status Eval) `seq` rv
          Forward for -> entForward for h `seq` 
                           case x of 
                             R y ry -> resForward for ry `seq` y)
       (case unsafePerformIO (readIORef status) of
          Hidden h -> let for = mkForward h 
                      in unsafePerformIO (writeIORef status (Forward for)) 
                         `seq` for
          Eval -> h) -- LOSE TRACE tv!

        
data Status = Hidden RefExp  -- neither value nor RefExp yet demanded
            | Forward RefExp -- RefExp demanded, value not yet
            | Eval           -- value demanded, RefExp not (yet?)     
\end{alltt}

If an untraced application is never evaluated, its trace is a Hidden node, otherwise its trace shall be the trace of the result of the evaluation.
The idea of \texttt{uwrapForward} is basically that it returns its second argument, but if the second argument is never evaluated, then the trace of the returned wrapper shall be the Hidden, which is passed as first argument. Any of the ``real'' value and the trace part of the wrapper may be demanded in any order or not at all. If the trace part is demanded first, a Forward node is created, which may later be updated when the ``real'' value is evaluated. However, if the ``real'' value is demanded first and later the trace part, then only Hidden is returned as trace. Hence values that are first demanded by trusted code and later demanded by traced code are not recorded in the trace.

\newpage
The obvious solution to the problem seems to be the following definition:

 \begin{alltt}
uwrapForward :: RefExp -> R a -> R a
uwrapForward h x =
  let status = unsafePerformIO (newIORef (Hidden h))
  in status `seq`
     R (case unsafePerformIO (readIORef status) of
          Hidden _ -> 
            case x of 
              R rv tv -> unsafePerformIO (writeIORef status \underline{(Eval tv)}) `seq` rv
          Forward for -> entForward for h `seq` 
                           case x of 
                             R y ry -> resForward for ry `seq` y)
       (case unsafePerformIO (readIORef status) of
          Hidden h -> let for = mkForward h 
                      in unsafePerformIO (writeIORef status (Forward for)) 
                         `seq` for
          \underline{Eval tv} -> \underline{tv}) 

        
data Status = Hidden RefExp  -- neither value nor RefExp yet demanded
            | Forward RefExp -- RefExp demanded, value not yet
            | \underline{Eval RefExp}    -- value demanded, RefExp not (yet?)     
\end{alltt}


However, with this definition we can no longer record cyclic data structures, for example the result of the standard function \texttt{repeat}:

\begin{alltt}
repeat x = let xs = x:xs in xs
\end{alltt}

Within the trace of a cyclic data structure there must be a Forward node, because only these can point forward in the trace. The last definition of \texttt{uwrapForward} does not record a Forward if the ``real'' value is demanded first and I do not see any way to introduce a Forward, in particular to call ``entForward'' and ``resForward''.

Alternatively, a Forward node could always be recorded, even if the trace is not demanded, but then we would be in the original situation that too much is recorded of a trusted computation, a Forward for every trusted application.

\section{The Crippled Forward Node}

The current definition of the Forward node in the trace is

$$Forward \{result :: RefEx\}$$

At first, $result$ points to the parent (a Hidden node), then becomes Unevaluated and finally points to any result trace. The problem is that the computation may be interrupted when Forward nodes are Unevaluated. These nodes are displayed as $\bot$ \emph{without} a parent. The internal stack still knows the parent, so that we obtain at least a useful start in hat-trail when such a Forward is the interrupted expression.

A simple solution is to let a Forward node have an extra bit in the tag. This bit is set when the node is entered while $result$ still points to the parent.


%------------------------------------------------------------------------------
\end{document}
