-\section*{Fleet Assembly Language}
-
-The Fleet Assembly language is designed to be a human-readable
-depiction of the bits which comprise a Fleet program. The formal
-syntax is given below:
-
-\verbatiminput{fleet.g}
-
-\pagebreak
-\section*{FleetDoc}
-
-Inspired by JavaDoc, the Fleet software toolchain includes a tool
-called {\tt FleetDoc}, which processes {\it ship description files}
-(with the extension {\tt .ship}). These files contain sections for:
-
-\begin{itemize}
-\item The name of the ship
-\item A list of its ports
-\item A prose description of the ship
-\item A list of the constants associated with a ship
-\item Java source code for a software simulation of the ship
-\item Verilog source code for an FPGA simulation of the ship
-\item A test case for the ship
-\item A list of the contributors to all of the above
-\end{itemize}
-
-Keeping all of this information in a single file ensures that changes
-to one item (such as the list of ports) are propagated to the other
-items (such as the verilog code for simulation purposes).
-
-Keeping this information in {\it machine-readable} format makes it
-possible to automatically generate tools which depend on the precise
-details of ship ports (such as the Fleet assembler) without the risk
-inherent in manual synchronization of the spec with the
-implementation.
-
-The latter half of this manual is generated automatically from the
-contents of the {\tt .ship} files.
-
-\pagebreak
-\subsection*{An Example FleetDoc File}
-\begin{verbatim}
-ship: BitFifo
-
-== Ports ===========================================================
-in: in
-in: inOp
- constant lsbFirst: ....................................1
- constant msbFirst: ....................................0
- constant drop: .............................uuuuuu..
- constant take: .......................uuuuuu........
-...
-
-== TeX ==============================================================
-The BitFifo internally stores some number of bits in a fifo structure.
-Its capacity is guaranteed to be at least two full machine words or
-more.
-...
-
-== Fleeterpreter ====================================================
-public void service() {
- if (box_inOp.dataReadyForShip() && box_in.dataReadyForShip()) {
- ...
-
-== FPGA ==============================================================
-always @(posedge clk) begin
- if (!in_r && in_a) in_a <= 0;
- if (!inOp_r && inOp_a) inOp_a <= 0;
- ...
-
-== Test ==============================================================
-#expect 1
-#expect 68719476736
-#ship debug : Debug
-#ship bitfifo : BitFifo
-
-bitfifo.outOp: literal BitFifo.outOp[take=37]; [*] deliver;
-...
-
-== Contributors =========================================================
-Amir Kamil <kamil@cs.berkeley.edu>
-Adam Megacz <megacz@cs.berkeley.edu>
-\end{verbatim}
-
-
-\pagebreak
-\section*{Java APIs}
-\subsection*{Representing Code}
-\subsection*{Representing Ships}
-
-\pagebreak
-\section*{Misc}
-
-\begin{verbatim}
-- sequencing guarantees
-- codebag format
-- behavior when token arrives at data port, vice versa
-- overlapping codebags
-\end{verbatim}
-
-\pagebreak
-\section*{Future Directions}
-
-\subsection*{The Role of the Count Field}
+\section{Opcodes}
+
+Opcodes, as specified in \cite{am25}, are not yet implemented, but
+should be.
+
+\section{Bypasses}
+
+Bypasses, as specified in \cite{am27}, are not yet implemented, but
+should be.
+
+\section{Sequencing Guarantees}
+
+\addcontentsline{toc}{subsection}{Source Sequence Guarantee}
+If two packets leave the same source and have the same path, they will
+arrive at their common destination {\it in the same order in which
+ they left the source}. This assurance is referred to as the {\it
+ source sequence guarantee}.
+
+\addcontentsline{toc}{subsection}{Instruction Sequence Guarantee}
+CodeBags in memory consist of an unordered set of {\it fibers}. A
+fiber is an ordered set of instructions which all share the same
+instruction path, and therefore will be executed by the same pump.
+Any code which dispatches a codebag {\it must} ensure that the
+instructions within a fiber reach their pump in the order in which
+they appear in the fiber. This is known as the {\it instruction
+ sequence guarantee}. Typically the software dispatching a codebag
+will take advantage of the source sequence guarantee in order to
+fulfill the instruction sequence guarantee.
+
+\section{Code Bags}
+
+Code bags may overlap in memory. If the assembler determines that two
+code bags share a set of fibers, it may feel free to re-order those
+fibers in such a way that the code bags overlap, sharing memory words
+for these fibers. The codebag descriptors for the two bags will then
+have different addresses and/or sizes, but the ranges which they
+encompass will overlap.
+
+\subsection{Dispatching Code Bags}
+
+A codebag is ``dispatched'' by causing its constituent words to
+arrive at the data latch of some output port, and then causing that
+output port's pump to execute a {\tt send} (not {\tt sendto})
+instruction, which is encoded as {\tt Do=1,To=1}. Because
+instructions are encoded in such a way that their {\tt Instruction
+ Path} appears in the upper 11 bits, the {\tt send} mechanism will
+correctly route the instruction to a pump will execute it.
+
+Currently the {\tt inCBD} port of the {\tt Memory} ship is ideally
+suited for this purpose, although a similar effect can easily be
+achieved using the {\tt BitFifo} ship in conjunction with the {\tt
+ Memory} ship. The only disadvantage to this arrangement is that the
+{\tt out} port must execute {\tt send} a certain number of times, and
+that number of times is determined by the {\tt size} field of the
+codebag descriptor. Unfortunately this value is not known at compile
+time, so it cannot be encoded as a repeat count on the instruction at
+the {\tt out} port. The typical solution is to place a standing ({\tt
+ count=$\infty$}) {\tt send} instruction at the {\tt out} port of one
+{\tt Memory} ship, and reserve that ship exclusively for dispatching
+code bags.
+
+Note that instructions are encoded relative to a particular dispatch
+output port. That is, the {\tt Instruction Path} field of the
+instruction specifies a path to the desired execution pump -- but this
+path is also specified with respect to some source. Therefore the
+instruction can be correctly dispatched only from that particular
+source. However, it is fairly simple to write software which can
+``relocate'' a codebag by replacing the {\tt Instruction Path} fields
+as needed.
+
+\subsection{Tokens and Data Items}
+
+When a data item is sent to a destination which expects a token, such
+as an output port destination, the effect will be the same as if a token
+had been sent to that destination, and the data value will be lost.
+
+When a token is sent to a destination which expects a data item, such
+as a pump destination or an input port destination, the effect will be
+the same as if a data item {\it having an undefined value} were sent
+to that destination. In other words, the programmer has no completely
+reliable mechanism for distinguishing between tokens and data items.
+
+
+\section{Future Directions}
+
+\subsection{The Role of the Count Field}