maybe.tex 3.75 KB
\section{\texttt{\large maybe} Statement Semantics}
\label{sec-maybe}

To begin we provide an overview of the \texttt{maybe} statement's semantics
describing how it allows developers to structure uncertainty. We refer to
each of the values or code paths a \texttt{maybe} statement can choose from
as an \textit{alternative}.

\begin{figure}[t]
\begin{minted}[fontsize=\footnotesize]{java}
// Setting variables
int retryInterval = maybe 1-16;
String policy = maybe "auto", "quality", "perf";

// Function alternatives
@maybe
int myFunction(int a) { /* First alternative */ }
@maybe
int myFunction(int a) { /* Second alternative */ }

// Inlining evaluation code
maybe {
  ret = fastPowerHungryAlgorithm(input);
} or {
  ret = slowPowerEfficientAlgorithm(input);
} evaluate {
  return { "repeat": false,
           "score" : nanoTime() + powerDrain() }
}

\end{minted}

\vspace*{-0.1in}

\caption{\small\textbf{More \texttt{maybe} Statements}}

\label{fig-maybeexamples}

\vspace*{-0.1in}

\end{figure}

\subsection{Setting Variables}

Variables can be used to represent uncertainty. Examples include an integer
storing how often a timer should trigger communication with a remote server,
or a string containing the name of a policy used to coordinate multiple code
blocks throughout the app. Figure~\ref{fig-maybeexamples} shows examples of
an integer that can take on values between 1 and 16, and a string that be set
to either ``auto'', ``quality'', or ``perf''.

\subsection{Controlling Code Flow}

Code flow can also represent uncertainty. Examples include using multiple
algorithms to compute the same result or multiple code paths representing
different tradeoffs between performance, energy, and quality.
Figure~\ref{fig-example-maybe} shows the \texttt{maybe} statement in its
simplest form controlling execution of multiple code blocks. If multiple
alternatives are specified, the system chooses one to execute; if only one
alternative is specified, the system chooses whether or not to execute it.
Single-alternative \texttt{maybe} statements can encapsulate or reorganize
logic that does not affect correctness, but may (or may not) produce some
desirable objective.

Figure~\ref{fig-maybeexamples} shows several extensions of the \texttt{maybe}
statement providing syntactic sugar. \texttt{maybe} function annotations
allow uncertainty to be expressed at the function level, with the
alternatives consisting of multiple function definitions with identical
signatures. Finally, \texttt{maybe} statements that require custom evaluation
logic can include an \texttt{evaluate} block as shown in the final example.
\texttt{evaluate} blocks provide app-specific \textit{a posteriori} logic to
evaluate the selected alternative. The \texttt{evaluate} block must return a
single JSON object with two components: (1) a positive integer
\texttt{score}, with smaller being better; (2) and a boolean \texttt{repeat}
indicating whether the system must use the same alternative next time. Hints
and custom evaluation logic can also be applied to other types of
\texttt{maybe} statements through annotations.

While it should be possible to nest \texttt{maybe} statements, it may require
compiler support to provide guarantees about how \texttt{maybe} decisions are
maintained across multiple code blocks. As we gain more experience with our
rewrite-based prototype, described next in Section~\ref{sec-certainty}, we
will revisit the question of nesting in future compiler-driven \texttt{maybe}
systems.

As a final remark, note that structured uncertainty is not randomness.
Randomness weights multiple options statically---there is no right or wrong
choice. In contrast, the \texttt{maybe} statement indicates that during any
given execution one alternative may be the right choice---even if the
developer or system cannot yet identify it.