\section{Introduction}

% Taken almost identically from Ana's journal paper (first submission).

The purpose of the {\CDx} is to detect potential collisions of aircraft located by a radar device. We take the program discussed in~\cite{KHPPTV09} as a basis for the definition of our requirements. It uses a cyclic executive, and embeds the assumption that the radar collects (and buffers) a frame of aircraft positions that becomes available for input periodically. In each iteration, the \CDx:~(1)~reads a frame; (2)~carries out a voxel-hashing step that maps aircraft to voxels; (3)~checks for collisions in each voxel; and (4)~records and reports the number of detected collisions. Unlike~\cite{KHPPTV09}, we allow aircraft to enter or leave the radar frame.

Since the majority of the computation burden is in the checking for collisions in step~(3), we propose a version of the \CDx\ where this task is parallelised. As a result, we obtain an SCJ program that illustrates the features of SCJ Level 1. Our aim with the concurrent {\CDx} is, most of all, to provide a genuine and more representative Level 1 application. Due to the novelty of the SCJ paradigm and technology, such applications are still difficult to come by in the public domain. On the other hand, even though we are not specifying a particular radar system, concurrent collision detection is a reasonable target to improve the performance of such an application. The program code is available via \url{http://www.cs.york.ac.uk/circus/hijac/}.

A voxel is a volumetric element; all voxels together subdivide the entire space. The voxels in the {\CDx} superimpose a coarse 2-dimensional grid on the x-y plane with the height of a voxel extending along the entire z-axis. Thus, the altitude of aircraft is abstracted away. This reduces the number of necessary collision tests:~after mapping aircraft to the voxels that are intersected by their interpolated trajectories, it is sufficient to test for possible collisions within each voxel. Details of the algorithm can be found in \cite{KHPPTV09}.

The concurrent {\CDx} consists of a single mission that instantiates seven handlers. Figure~\ref{fig:ParallelCDxUML} presents a UML class diagram that illustrates the design. The classes shaded are part of the SCJ API. The classes \verb"CDxSafelet", \verb"CDxMissionSequencer" and \verb"CDxMission" implement the safelet, the mission sequencer, and the mission. The behaviour of the \verb"setUp()" and \verb"tearDown()" methods of \verb"CDxSafelet" is void, and \verb"getSequencer()" simply returns an instance of \verb"CDxMissionSequencer". Likewise, \verb"getNextMission()" returns an instance of \verb"CDxMission" when called for the first time. Since the mission does not terminate, \verb"getNextMission()" is not called again.

\begin{figure}[t]
  \centering
  \includegraphics*[scale=0.83,trim=150 160 150 150]{ParallelCDxUML.pdf}
  \caption{UML diagram for the concurrent {\CDx} program}
  \label{fig:ParallelCDxUML}
\end{figure}

In the mission execution, first the \verb"initialize()" method of \verb"CDxMission" is called. It creates the handler objects and shared data in mission memory. The handler classes are \verb"InputFrameHandler", \texttt"OutputCollisions\-Handler", \verb"ReducerHandler", and \verb"DetectorHandler". We choose to create four instances of \verb"DetectorHandler", possibly corresponding to a scenario in which we have four processors. The refinement in the remainder of the report can, however, proceed without significant changes in the presence of a different number of instances. A more general design for the \CDx\ could allow the configuration of the number of instances; our program, however, is enough to illustrate the main aspects of our technique.

The shared data is held by public fields of \verb"CDxMission". The \verb"currentFrame" and \verb"state" fields record the current and previous frame of aircraft positions; recording previous positions is important for calculating their predicted motions. As we divide and distribute the computational work, \verb"work" holds the partitions of voxels to be checked by each of the detection handlers, and \verb"collisions" is used to accumulate the result of the detection. Another shared object \verb"control" plays a crucial part in orchestrating the execution of handlers.

Figure~\ref{fig:ParallelCDxControl} summarises the control mechanism of the SCJ application. The three software events, \verb"reduce", \verb"detect" and \verb"output", are used to control execution of the handlers. The program design ensures that the handlers effectively execute sequentially in each cycle, apart from the four instances of \verb"DetectorHandler", which carry out their work concurrently.

\begin{figure}[t]
  \centering
  \includegraphics*[scale=0.8,trim=135 155 155 165]{ParallelCDxControl.pdf}
  \caption{Parallel {\CDx} control flow}
  \label{fig:ParallelCDxControl}
\end{figure}

The \verb"InputFrameHandler" is the only periodic handler. It is released at the beginning of each cycle to interact with the hardware to read the frame into \verb"currentFrame" and update \verb"state" accordingly. Afterwards, it releases the \verb"ReducerHandler", via the \verb"reduce" software event, to carry out the voxel-based reduction step. This handler also partitions and distributes the work among the detector handlers by populating \verb"work". Once this is done, it concurrently releases all \verb"DetectorHandler" instances by firing the \verb"detect" event. These handlers carry out the actual detection work and store their result in \verb"collisions". The mechanism for releasing \verb"OutputCollisionsHandler", which outputs the number of collisions to an external device, uses the shared object \verb"control". Its class type \texttt{DetectorControl} provides a method \texttt{notify(int id)}, which is called by the detector handlers at the end of each release. It fires the event \texttt{output} when all detection work is done. This illustrates that sharing may occur not only to exchange data between handlers, but also in the design of execution control, and our refinement strategy will have to cater for this.

Our program highlights various features of the SCJ mission framework:~the subdivision of a mission into handlers, the control of handlers via software events, and the sharing of data for both data communication and control purposes. The verification of this program not only has to address functional correctness, but also must show that the flow of activities in Figure~\ref{fig:ParallelCDxControl} can be executed within the duration of a cycle.
