\section{Introduction}
\label{sec:intro}

Many industrial applications, including safety-critical ones, consist of several disjoint components that use message passing to communicate according to some protocol. These components are typically highly concurrent, since messages may be sent and received in any order. Developing functionally correct message passing programs is therefore very challenging, which makes proving their correctness crucial~\cite{hoare:2008verified}.

The Message Passing Interface (MPI) is a popular API for implementing message passing programs. We focus on the modular verification of MPI programs, in particular programs written with Java and the MPJ library~\cite{mpj:2016url}. Existing research mainly focusses on proving communication correctness over an abstract system model~\cite{hoare2008:separation,vo:2009formal}. Instead, we target concrete Java source code and combine well-known techniques for static verification with process algebras to reason about communication correctness~\cite{milner:1980calculus}. Communication correctness refers to the correctness of handling messages, i.e. freedom of deadlocks and livelocks, resource leakage, proper matching of sends and receives, etcetera.

Global system correctness depends on the correctness of all individual processes and their interactions. We use permission-based separation logic~\cite{o:2007resources} to statically reason about local correctness. In addition, we model the communication protocol in the mCRL2 process algebra. We refer to these algebraic terms as \emph{futures} as they predict how components will interact during program execution~\cite{zaharieva:2015closer}\footnote{Not to be confused with the concepts of ``futures and promises" used in MultiLisp, described by Halstead~\cite{halstead:1985multilisp} and Liskov and Shrira~\cite{liskov:1988promises}.}. We extend the VerCors toolset~\cite{amighi:2014verification,blom:2014vercors} to establish a provable link between futures and program code so that reasoning about futures corresponds to reasoning about the concrete program. Analysing futures can then be reduced to a parameterised model checking problem to reason about the functional and communication correctness of the system. Since model checkers inherently target finite-state systems, we use abstraction and cut-offs to reason about programs with infinite behaviour whenever possible.

In this paper we analyse the behaviour of several standard MPI operations and model their semantics as process algebra terms. We define several actions, like \textbf{send}, \textbf{recv}, and \textbf{bcast}, that can be used in futures to specify process communication, like that done with Session Types~\cite{honda:2012verification}. After that, we show how to analyse futures, in combination with the process algebra terms that model the semantics of the MPI runtime. The analysis is done via parameterised model checking, for which we plan to use the mCRL2 toolset~\cite{groote:2014modeling}. The key element of our approach is that, by verifying safety and liveness properties on the futures, we actually verify equivalent properties on the concrete system of \emph{any} size. This allows us to check whether process communication always leads to a valid system state in every system configuration. We also plan to check other interesting safety and liveness properties, including: deadlock freedom, resource leakage, and global termination.

This paper is organised as follows. \autoref{sec:mpi} introduces the message passing paradigm and discusses the semantics of several standard MPI operations. \autoref{sec:comm} contributes an algebraic abstract model of the network environment. \autoref{sec:link} shows how futures and the abstract network environment are used to reason about concrete program code. \autoref{sec:example} demonstrates our approach by verifying a leader election protocol. Finally, \autoref{sec:conclusions} summarises our conclusions and presents future work.

\section{The message passing paradigm}
\label{sec:mpi}

MPI programs consist of a group of interconnected processes $(p_0, \dots, p_{N-1})$ distributed over one or more devices connected via some network. Each process $p_j$ executes the same program in Single Program Multiple Data (SPMD) fashion, in which $j$ is called the \emph{rank} and $N$ the \emph{size}. MPI mainly targets distributed memory systems; processes maintain a private memory and accesses to non-local memories are handled exclusively via message exchanges. Verifying MPI programs involves verifying functional and communication correctness for \emph{every} rank and size.

The MPI standard describes a set of subroutines to allow processes to exchange messages. We briefly discuss several standard point-to-point and collective MPI operations and their semantics.

\vspace{-8pt}
\paragraph{Standard operations.}
A process $p_i$ can send a message with data element $D$ to process $p_j$ by calling $p_i.\texttt{MPI\_Send}(j, D)$. Similarly, $p_i$ may receive a message from $p_j$ with content $D$ by invoking $D := p_i.\texttt{MPI\_Recv}(j)$. We remove the prefix ``$p_i$." if the sending process can be inferred from the context. Every $\texttt{MPI\_Send}$ must be matched by a $\texttt{MPI\_Recv}$. We allow wildcard receives, i.e. calling $p_i.\texttt{MPI\_Recv}(\star)$ to receive from any process. In this paper we omit tags and communicators.

The MPI standard describes four sending modes for point-to-point communication, namely: blocking mode, buffered mode, synchronous mode, and ready mode. The $p_i.\texttt{MPI\_Send}(j,D)$ operation is a blocking mode send, as it \emph{may} block $p_i$ until matched by a call $p_j.\texttt{MPI\_Recv}(i)$. The buffered variant, $p_i.\texttt{MPI\_BSend}$, does not block $p_i$ until matched by a \texttt{MPI\_Recv} if the request can be buffered. The synchronous variant, $p_i.\texttt{MPI\_SSend}$, \emph{always} blocks $p_i$ until matched by a \texttt{MPI\_Recv}. Finally, the ready mode variant, \texttt{MPI\_RSend}, only succeeds if a matching \texttt{MPI\_Recv} has already been posted. From now, we only consider the blocking mode \texttt{MPI\_Send} variant to illustrate our approach. In future work we also provide support for the other three communication modes.

\vspace{-8pt}
\paragraph{Non-blocking variants.}
The immediate send, \texttt{MPI\_ISend}, is an immediate variant on the standard blocking send. Calling $r := p_i.\texttt{MPI\_ISend}(j,D)$ is \emph{not} allowed to block $p_i$ for a matching \texttt{MPI\_Recv} by $p_j$. Instead, \texttt{MPI\_ISend} returns a request handle $r$ which can be used to query or influence the status of the request. The operation $p_i.\texttt{MPI\_Wait}(r)$ blocks $p_i$ until the operation corresponding to the handle $r$ has been completed. Two consecutive non-blocking calls $p_i.\texttt{MPI\_ISend}(j, \star)$ and $p_i.\texttt{MPI\_ISend}(k, \star)$ made by process $p_i$ are \emph{forced} to match in order if $j=k$, but may be handled in \emph{any} order if $j \not = k$.

Apart from the immediate blocking send, also the other three sending modes have immediate variants, which are: \texttt{MPI\_IBsend}, \texttt{MPI\_ISsend}, and \texttt{MPI\_IRsend}. In this paper we only focus on \texttt{MPI\_ISend}. In future work we provide support for the other three immediate operations.

\vspace{-8pt}
\paragraph{Collective operations.}
The collective $p_i.\texttt{MPI\_Barrier}()$ operation blocks execution of $p_i$ until matched by a call $p_j.\texttt{MPI\_Barrier}()$ for every $j \not = i$ and can therefore be used to synchronise all processes. Non-blocking operations invoked before calling $\texttt{MPI\_Barrier}$ may complete while lingering in the barrier, as they are handled by the network environment. We plan to provide support for other collective operations, like: $\texttt{MPI\_Reduce}$, $\texttt{MPI\_Scatter}$, and $\texttt{MPI\_Gather}$, but this is future work. The collective $p_i.\texttt{MPI\_Bcast}(D)$ operation is used to broadcast a data element $D$ to every participating process. For now we assume that $p_i.\texttt{MPI\_Bcast}(D)$ simply calls $p_i.\texttt{MPI\_Send}(j, D)$ for every $j \not = i$.

\section{Modelling the communication network}
\label{sec:comm}

We use futures to predict the communication protocol of MPI programs. In this section we specify abstract actions, e.g. $\textbf{send}$, $\textbf{recv}$, and $\textbf{bcast}$, that correspond to concrete MPI operations. We also model the network environment and thereby the semantic behaviour of the MPI operations. Futures are constructed via the following syntax, which is a subset of the multi-action process algebra used in mCRL2, proposed by Groote and Mousavi~\cite{groote:2014modeling}:

\vspace{-2pt}
$$P ::= \textbf{a} ~|~P + P ~|~ P \cdot P ~|~ P \parallel P ~|~ c \rightarrow P ~|~ c \rightarrow P \diamond P ~|~ \sum_{d \in T} P(d) ~|~ \textsf{X}(u_1, \dots, u_n)$$

\vspace{-1pt}
Actions have the form $\textbf{a} : T_1 \times \cdots \times T_n$, where all $T_i$ are types, e.g. sets, maps, integers, sequences, and so on. We include $\tau$ as a special silent action. Sequential composition is denoted by $P \cdot P'$ ($P$ is executed before $P'$) and choice is denoted by $P + P'$ (either $P$ or $P'$ is executed). Summations $\sum_{d\in T}P(d)$ of choices are also supported, where $P$ is executed for some model $d$ of type $T$. The expression $P \parallel P'$ means putting $P$ and $P'$ in parallel, thereby allowing their actions to be interleaved. Conditions are written either as $c \rightarrow P$ (execute $P$ only if $c$ is true) or $c \rightarrow P \diamond P'$ (execute $P$ if $c$ is true, otherwise execute $P'$). Finally, $\textsf{X}(u_1, \dots, u_n)$ calls a process $\textsf{X}$ with a list of $n$ arguments of appropriate types.

Two actions $\textbf{a},\textbf{b}$ may communicate by specifying a \emph{communication pair}, written $\textbf{a}|\textbf{b}$. Two communicating actions are forced to happen simultaneously and thereby impose restrictions on the evaluation of actions. As an effect, communication pairs introduce synchronisation points between processes.

\vspace{-4pt}
\paragraph{Modelling the network environment.}
Recall that MPI programs are executed on a group of $N$ processes $(p_0, \dots, p_{N-1})$. Let $\mathcal{R} = \{0, \dots, N - 1\}$ be the set of ranks. The network can be modelled as a collection of queues that store pending messages, i.e. messages sent but not yet received. Therefore, we model the network environment as a recursive process, named \textsf{Network}, that maintains a set $T = \{ Q_{i,j} \ | \ i,j \in \mathcal{R} \}$ of queues $Q_{i,j}$ for each pair of ranks $i,j \in \mathcal{R}$ to maintain the state of the network. \textsf{Network} is defined as follows, where $\mathcal{M}$ denotes the set of all possible messages:

\vspace{-8pt}
\begin{equation*}
	\begin{split}
		\textbf{process} \ \textsf{Network}(T) \equiv \sum_{i,j\in\mathcal{R}} & \sum_{m \in \mathcal{M}} \Big( \textbf{nrecv}(i,j,m) \cdot \textsf{Network}(T.enqueue(i, j, m)) \ + \ \\
		&T.peek(i, j, m) \rightarrow \textbf{nsend}(j,i,m) \cdot \textsf{Network}(T.dequeue(i, j)) \Big)
	\end{split}
\end{equation*}

Observe that \textsf{Network} uses two actions, namely: (1) \textbf{nsend} for sending a message from the network to a process; and (2) \textbf{nrecv} for receiving a message from a process. Processes may use the network by communicating with these two actions. More specifically, we define two actions, \textbf{send} and \textbf{recv}, that correspond to the functions \texttt{MPI\_Send} and \texttt{MPI\_Recv}, respectively. Standard blocking-mode sends and receives are performed via the communication pairs $\textbf{send}|\textbf{nrecv}$, $\textbf{recv}|\textbf{nsend}$, and $\textbf{send}|\textbf{recv}$. For the immediate blocking send, \texttt{MPI\_ISend}, we also define a corresponding action $\textbf{isend}$ and use the communication pair $\textbf{isend}|\textbf{nrecv}$. Moreover, the $T.enqueue(i,j,m)$ and $T.dequeue(i,j)$ functions are just auxiliary functions used to enqueue/dequeue elements from $Q_{i,j}$, which can easily be specified in mCRL2. In the remaining of this paragraph, we give more detail on the abstract actions and communication pairs.

When a future performs the $\textbf{send}(i,j,m)$ action, which corresponds to a call $p_i.\texttt{MPI\_Send}(j, m)$ in the program code, the network may receive the message via communication with $\textbf{nrecv}(i,j,m)$, i.e. by having the communication pair $\textbf{send}|\textbf{nrecv}$. After communication, the message is stored in the network by applying $T.enqueue(i,j,m)$, which enqueues $m$ onto $Q_{i,j}$. Similarly, the $\textbf{recv}(i,j,m)$ action, which corresponds to the invocation $m := p_i.\texttt{MPI\_Recv}(j)$, communicates with $\textbf{nsend}$, i.e. $\textbf{recv}|\textbf{nsend}$. The network environment can send a message $m$ to process $p_i$ via the $\textbf{nsend}(i,j,m)$ action if $p_i$ chooses to communicate with the network via a matching $\textbf{recv}(i,j,m)$ action. The network can only send the top element of $Q_{i,j}$ as the MPI standard enforces a FIFO order, hence the check $T.peek(i,j,m)$, which returns true only if $m$ is the top element of $Q_{i,j}$. When $p_i$ chooses to receive the message $m$, the queue $Q_{i,j}$ is updated by dequeuing the message $m$, which is done by applying $T.dequeue(i,j,m)$. Since $p_i.\texttt{MPI\_Send}$ \emph{may} block $p_i$ until matched by a \texttt{MPI\_Recv} but is not forced to do so, we also allow \textbf{send} to communicate directly with \textbf{recv}, i.e. having the communication pair $\textbf{send}|\textbf{recv}$, thereby bypassing the network process.

For the immediate blocking send, \texttt{MPI\_ISend}, we define a corresponding action $\textbf{isend}$, so that calling $r := p_i.\texttt{MPI\_ISend}(j, D)$ corresponds to $\textbf{isend}(i,j,m,r)$. The $\textbf{isend}$ action can not directly communicate with $\textbf{recv}$ and therefore \emph{only} communicates via the network: $\textbf{isend}|\textbf{nrecv}$. Note that two consecutive actions $\textbf{isend}(i, j, m, r)$ and $\textbf{isend}(i, k, m', r')$ performed by rank $i$ match in order if $j=k$, since $m$ and $m'$ are consecutively added to the same queue $Q_{i,j}=Q_{i,k}$ and thus handled in that specific order. The two actions may perform in any order if $j\not=k$, as they are added to different queues $Q_{i,j} \not = Q_{i, k}$.

To support other send modes, the \textsf{Network} process is still too simple. For example, to support the buffered sends \texttt{MPI\_Bsend} and \texttt{MPI\_IBsend}, buffer space needs to be taken into account, which may potentially break the FIFO ordering. Ready-mode sends require extra checks to ensure that the network already contains a matching receive. Synchronous-mode sends only allow direct synchronisations, e.g. having the communication pair $\textbf{ssend}|\textbf{recv}$, where \textbf{ssend} corresponds to \texttt{MPI\_Ssend}.

\vspace{-4pt}
\paragraph{Short example of network interaction.}
To illustrate the use of multi-actions to communicate with the network environment, we give a short producer/consumer example. Suppose that the network is used by two processes: (1) a producer that only sends messages; and (2) a consumer that only receives messages sent by the producer. The producer and consumer are defined as follows:

$$\textbf{process}~\textsf{Producer}(v:\mathbb{Z}) \equiv \textbf{send}(0, 1, v) \cdot \textsf{Producer}(v + 1)$$
$$\textbf{process}~\textsf{Consumer}(t:\mathbb{Z}) \equiv \sum_{n \in \mathbb{Z}} \textbf{recv}(1, 0, n) \cdot \textsf{Consumer}(t + n)$$

Consider the initial configuration $\textsf{Producer}(0) \parallel \textsf{Consumer}(0) \parallel \textsf{Network}(T_{\emptyset})$, where $T_{\emptyset}$ denotes the set of empty queues, i.e. $|Q_{i,j}| = 0$ for every $Q_{i,j} \in T_{\emptyset}$. From the initial configuration, the only allowed transition is the multi-action $\textbf{send}|\textbf{nrecv}$, which results into the configuration $\textsf{Producer}(1) \parallel \textsf{Consumer}(0) \parallel \textsf{Network}(T')$, where $T'$ is equal to $T_{\emptyset}$, but with $0$ enqueued onto $Q_{0,1}$. From this configuration, either $\textbf{send}|\textbf{nrecv}$ (the producer sends another value to the network) or $\textbf{recv}|\textbf{nsend}$ (the consumer receives a value from the network) may happen, and this process repeats forever.

\vspace{-4pt}
\paragraph{Modelling broadcasts and barriers.}
For broadcasting we define the action $\textbf{bcast}(i,m)$ that corresponds to the function call $p_i.\texttt{MPI\_Bcast}(m)$. Broadcasts are handled by a separate process, called $\textsf{Bcast}$, dedicated to transform a call $p_i.\texttt{MPI\_Bcast}(m)$ into a series of calls $p_i.\texttt{MPI\_Send}(j, m)$ for every $j \not = i$. The $\textsf{Bcast}$ process is defined as follows:

\vspace{-8pt}
\begin{equation*}
	\begin{split}
		\textbf{process} \ \textsf{Bcast}() &\equiv \sum_{i \in \mathcal{R}} \sum_{m \in \mathcal{M}} \Big( \textbf{breq}(i, m) \cdot \textsf{Handle}(i,m,\mathcal{R}\backslash \{i\}) \Big) \\
		\textbf{process} \ \textsf{Handle}(i,m,R) &\equiv (R \not = \emptyset) \rightarrow \sum_{j \in R} \Big( \textbf{nsend}(i,j,m) \cdot \textsf{Handle}(i,m,R \backslash \{j\}) \Big) \diamond \textsf{Bcast}()
	\end{split}
\end{equation*}

When a future starts broadcasting by performing $\textbf{bcast}(i,m)$, the \textsf{Bcast} process receives the broadcast request by communicating with $\textbf{breq}$, i.e. via the communication pair $\textbf{bcast}|\textbf{breq}$. The \textsf{Handle} process actually handles the broadcast request by generating a $\textbf{nsend}(i,j,m)$ action for every $j \not = i$. Any process $p_j$ may then receive the message $m$ by communicating via a standard \textbf{recv} action. Note that $\textsf{Handle}(i,m,R)$ only calls $\textsf{Bcast}$ if all ranks $j \in \mathcal{R} \backslash \{i\}$ have synchronised on $\textbf{nsend}(i,j,m)$.

For handling barriers we define the action $\textbf{barrier}(i)$ that corresponds to the call $p_i.\texttt{MPI\_Barrier}()$. Similar to broadcasts, also barriers are handled by a dedicated process, named \textsf{Barrier}, which simply synchronises with the $\textbf{barrier}$ action. In particular, performing an action $\textbf{barrier}(i)$ prevents further actions to be executed until $\textsf{Barrier}$ has synchronised with $\textbf{barrier}(j)$ for every $j \not = i$. We omit the definition of \textsf{Barrier}, as it is essentially the same as \textsf{Bcast}.

\section{Linking futures to program code}
\label{sec:link}

We use permission-based separation logic~\cite{o:2007resources} to reason about local correctness of MPI programs. We include the permissions, since we allow MPI processes to create threads. In particular, we assume that MPI programs $S$ have preconditions $P$ and postconditions $Q$, so that partial correctness can be proven via Hoare triples $\{P\} S \{Q\}$. The conditions $P$ and $Q$ may then use permissions to guarantee data-race freedom in case of multi-threading.

\vspace{-4pt}
\paragraph{Hoare triple reasoning.}
To find a correspondence between program code and futures, we use Hoare triple reasoning. More specifically, we extend Hoare triples to verify that an MPI program satisfies its algebraically predicted behaviour. For example, we may specify a future: ``$\textbf{send}(i,j,m) \cdot \textbf{recv}(j,i,n)$'' that predicts the behaviour of the program fragment: ``$p_i.\texttt{MPI\_Send}(j, m); ~n := p_i.\texttt{MPI\_Recv}(j)$''. We prove a link between the future and the program fragment via the Hoare triples: $\{ \textbf{send}(i,j,m) \cdot \textbf{recv}(j,i,n) \cdot \textsf{F} \} p_i.\texttt{MPI\_Send}(j, m) \{ \textbf{recv}(j,i,n) \cdot \textsf{F} \}$ and $\{ \textbf{recv}(j,i,n) \cdot \textsf{F} \} n = \texttt{MPI\_Recv}(j) \{ \textsf{F} \}$, where $\textsf{F}$ describes the future of the remaining program. To generalise, for the \textbf{send}, \textbf{recv}, \textbf{bcast}, and \textbf{barrier} actions we use the following four Hoare triple axioms: \\

\noindent
{
\small
\begin{tabular}{ll}
	$$\inference[\text{[send]}~:~]{}{\{ \textbf{send}(i,j,m) \cdot \textsf{F} \} p_i.\texttt{MPI\_Send}(j,m) \{ \textsf{F} \}}$$ & $$\inference[\text{[recv]}~:~]{}{\{ \textbf{recv}(i,j,m) \cdot \textsf{F} \} m := p_i.\texttt{MPI\_Recv}(j) \{ \textsf{F} \}}$$ \\
\end{tabular}
} \\

\noindent
{
\small
\begin{tabular}{ll}
	$$\inference[\text{[bcast]}~:~]{}{\{ \textbf{bcast}(i,m) \cdot \textsf{F} \} p_i.\texttt{MPI\_Bcast}(m) \{ \textsf{F} \}}$$ & $$\inference[\text{[barrier]}~:~]{}{\{ \textbf{barrier}(i) \cdot \textsf{F} \} p_i.\texttt{MPI\_Barrier}() \{ \textsf{F} \}}$$ \\
\end{tabular}
}

\vspace{12pt}
All other actions that correspond to MPI functions, e.g. immediate sends like \textbf{isend}, alternative send modes like \textbf{ssend}, \textbf{bsend}, etcetera, are proven to correspond to the MPI program in the same way. We extend the VerCors toolset to verify these Hoare triples by specifying appropriate triples to handle sequential composition of futures: $\textsf{F} \cdot \textsf{G}$, choices between futures: $\textsf{F} + \textsf{G}$, and so on.

\paragraph{Splitting futures.}
Since we allow multi-threading, we use permission-based separation logic to prove local correctness of MPI programs. The process algebraic equivalent to multi-threading is the parallel composition: $\textsf{F} \parallel \textsf{G}$. We assign permissions to futures, written ``$\text{Future}(\pi, \textsf{F})$'', meaning that a permission fragment $\pi$ is assigned to the future $\textsf{F}$. Then we allow splitting and merging of futures: ``$\text{Future}(\pi_1 + \pi_2, \textsf{F} \parallel \textsf{G}) *-* \text{Future}(\pi_1, \textsf{F}) * \text{Future}(\pi_2, \textsf{G})$'' in separation logic style. The splitted futures can then be distributed among parallel threads, where the permissions can be used for allocating resource invariants.

We refer to the initial future as the \emph{global} future, since it has full permission. The global future can be split into \emph{local} futures with fractional permissions. Proving correctness of local futures with respect to a program fragment is done via standard Hoare logic reasoning~\cite{zaharieva:2015closer}.
For example, the algorithm in \autoref{fig:protocol}, which is discussed in detail in \autoref{sec:example}, shows how program code is annotated with futures. In \autoref{fig:protocol}, all futures have full permission since the algorithm does not fork additional threads.

\vspace{-4pt}
\paragraph{Communication correctness.}
Let $P$ be an MPI program and $\textsf{F}$ its predicted global future. If we can prove that $P$ correctly executes according to $\textsf{F}$ (i.e. proving $\{ \textsf{F} \}P \{ \epsilon \}$ for the empty process $\epsilon$), then we need to analyse $\textsf{F} \parallel \cdots \parallel \textsf{F}$ to reason about functional and communication correctness of the network of processes all running $P$. Let $\textsf{F}^n = \textsf{F} \parallel \cdots \parallel \textsf{F}$ be the parallel composition of $n$ futures $\textsf{F}$. In particular, we need to verify correctness of $\textsf{F}^N$ for \emph{every} size $N$, in combination with the network environment. Therefore, we will use mCRL2~\cite{mcrl2:2016url} to analyse the following configuration, where $T_{\emptyset}$ denotes the set of empty queues:
$$\textsf{F}^N \parallel \Big( \textsf{Network}(T_{\emptyset}) \parallel \textsf{Bcast}() \parallel \textsf{Barrier}() \Big)$$

\section{Example: A leader election protocol}
\label{sec:example}

We illustrate our approach on a small example with $N$ processes $(p_0, \dots, p_{N-1})$ performing a leader election protocol. The processes communicate in a ring topology, so that process $p_i$ only sends messages to $p_{i + 1}$ and only receives messages from $p_{i-1}$, counting modulo $N$. Each process $p_i$ holds a \emph{unique} integer $v_i$ so that $v_i \not = v_j$ for $i \not = j$. The leader is the process $p_j$ with the highest value $v_j$, that is, $v_j = max \{ v_0, \dots, v_{N-1} \}$. The protocol operates in a number of rounds. In each round, each process circulates and remembers its highest encountered value. Ultimately, after $N$ rounds, all processes know the highest participating value $v_j$ and the leader announces itself by broadcasting its rank.

\begin{figure}[t]
	\centering
	\input{example.tex}
	\vspace{-8pt}
	\caption{Annotated example program of a leader election protocol with simplified MPI syntax.}
	\vspace{-2pt}
	\label{fig:protocol}
\end{figure}

\autoref{fig:protocol} shows annotated pseudocode. The program distinguishes between two kinds of messages: $\color{blue}\texttt{elect}\langle n \rangle$ for communicating an integer $n \in \mathbb{Z}$, and $\color{blue}\texttt{lead}\langle j \rangle$ for communicating a rank $j \in \mathcal{R}$. Below the predicted futures $\textsf{Elect}$ and $\textsf{Choose}$ are given for $\texttt{election}$ and $\texttt{chooseLeader}$, respectively.

\vspace{-4pt}
\begin{equation*}
	\begin{split}
		\textbf{process} & \ \textsf{Elect}(i,v,h,n) \equiv (n < N) \rightarrow  \sum_{h' \in \mathcal{M}} \Big( \textbf{send}(i,i+1 ~\text{mod}~ N,{\color{blue}\texttt{elect}\langle h \rangle}) \\ & \cdot \textbf{recv}(i - 1 ~\text{mod}~ N, i, {\color{blue}\texttt{elect}\langle h' \rangle}) \cdot \textsf{Elect}(i, v, max(h,h'), n + 1) \Big)  \diamond \textsf{Choose}(i,h,v) \\
		\textbf{process} & \ \textsf{Choose}(i,h,v) \equiv \Big( (h=v) \rightarrow \textbf{bcast}(i, {\color{blue} \texttt{lead} \langle i \rangle}) ~\diamond~ \sum_{j \in \mathcal{R}} \textbf{recv}(j,i,{\color{blue}\texttt{lead} \langle j \rangle}) \Big) \cdot \textbf{barrier}(i)
	\end{split}
\end{equation*}

Assume that each process $p_i$ is started by invoking $\texttt{election}(v_i, v_i, 0)$ and therefore starts with the initial future $\textsf{Elect}(i, v_i, v_i, 0)$. We \emph{predict} with \textsf{Elect} that $p_i$ sends the value $h$ to process $p_{i+1}$ in an $\color{blue}\texttt{elect}$ message, receives a value $h'$ from process $p_{i-1}$ as an $\color{blue}\texttt{elect}$ message, and repeats this process as long as $n < N$ while considering $h \gets max(h, h')$. After $N$ rounds we predict the leader $p_j$ to broadcast its rank by sending a $\color{blue}\texttt{lead}\langle j \rangle$ message and all other processes $p_i$ to receive the $\color{blue}\texttt{lead} \langle j \rangle$ message.

By observing the code, a leader is elected by circulating all values $v_i$ through the ring topology in $N$ rounds, hence the check at \autoref{line:reccheck}. In each round, every process $p_i$ receives a message $\color{blue}\texttt{elect}\langle h' \rangle$ from $p_{i-1}$ (\autoref{line:recvelect}), where $h'$ is the maximum value encountered by $p_{i-1}$. In turn, $p_i$ send its highest encountered value $h$ to $p_{i+1}$ (\autoref{line:sendelect}). Finally, $h$ is updated (\autoref{line:updateh}) to remain the highest encountered value before starting the next round (\autoref{line:reccheck}). After $N$ rounds, each process $p_i$ invokes the function $\texttt{chooseLeader}(h,v)$. If $h = v$, then $p_i$ is the leader due to the uniqueness of the values $v_i$. The leader $p_j$ broadcasts its rank $j$ to all other processes via a $\color{blue}\texttt{lead} \langle j \rangle$ message (\autoref{line:bcastrank}). All other processes receive the rank of the leader (\autoref{line:recvrank}). Finally, all processes synchronise by entering a barrier.

The $\texttt{election}$ function is proven via the following Hoare triple: $\{ 0 \leq n \leq N \ \wedge \ v \leq h \ \wedge \ \textsf{Elect}(i,v,h,n) \cdot \textsf{F} \} p_i.\texttt{election}(h,v,n) \{ \textsf{F} \}$, with $p_i$ the executing process. Similarly, the $\texttt{chooseLeader}$ function is proven via the triple: $\{ h \geq v \ \wedge \ \textsf{Choose}(i,h,v) \cdot \textsf{F} \} p_i.\texttt{chooseLeader}(h,v) \{ \textsf{F} \}$. After that, we use mCRL2 to reason about the global state and thereby reason about program executions in a global setting. For example, we may verify that the invocation $\texttt{chooseLeader}(h,v_i)$ receives a parameter $h \in \mathbb{Z}$ such that $h = max \{v_0, \dots, v_{N-1} \}$ and $h = v_j$ for exactly one $j \in \mathcal{R}$. In particular, we verify that the leader $p_j$ eventually broadcasts the message $\color{blue}\texttt{lead}\langle j \rangle$ containing its rank, and that all other processes eventually receive that message. In that case, all processes receive the rank of the leader and communicate correctly according to the predicated future.

\section{Conclusion and future work}
\label{sec:conclusions}

The work described in this paper is still in its early stages. We have already manually worked out a couple of verification examples, including the leader election protocol described in \autoref{sec:example}. We are currently working on providing tool support by extending the VerCors toolset. In particular, we define new Hoare triples to handle futures in combination with the abstract MPI actions described in \autoref{sec:comm}. Moreover, we are extending the network environment to support more MPI functions, like: \texttt{MPI\_Scatter}, \texttt{MPI\_Gather}, and \texttt{MPI\_Reduce}, which are focused on distributing data in a specific way. After extending VerCors we plan to make a connection with mCRL2 for future-based analysis of the global system consisting of $N$ instances of the program. Finally, we plan to show correctness of some industrial message passing programs in a case study. \\

\noindent
{\large \textbf{Acknowledgements.}} Oortwijn is funded by the NWO TOP project VerDi (projectnr. 612.001.403). Blom and Huisman are funded by the ERC 258405 VerCors project.

\nocite{*}
\bibliographystyle{eptcs}
\vspace{-8pt}


\section{INTRODUCTION}

\iffalse

\fi

Lane and road markings are critical elements in traffic scenes. The lane lines or road signs such as arrows can provide valuable information for self-driving cars' planning and controlling.

Current lane marking detection methods mostly utilize the segmentation technique~\cite{VPGNet}\cite{LaneNet}\cite{SpatialCNN}, which is based on fully convolutional deep neural networks (FCNs).
The segmentation networks rely on local features which are extracted from the raw RGB pattern and mapped into semantic spaces for pixel-level classification. However, such an architecture often suffers from an accuracy degradation for lane and road markings far away from the ego-vehicle, because these markings occupy a small number of pixels in the image, and their features become inconsistent for varying distances and perspectives, as shown in Fig.~\ref{fig:lanemarking_illustration}.
, while both distant and close lane marking information is important for the controlling and planning tasks.
\begin{figure}[tbp]
    \centering
    \includegraphics[width=\linewidth]{0209.png}
    \caption{View of the lane markings at different distances. Similar lane markings in bird's eye view show very different shape and scale features in original view.}
    \label{fig:lanemarking_illustration}
    \end{figure}

An intuitive solution is to transform the original image to a bird's-eye view (BEV) using the Inverse Perspective Mapping (IPM). In principle, this can solve the problem of inconsistent scales of road markings at different distances. However, the IPM is typically implemented by interpolation which reduces the resolution of the distant road surface and create unnatural blurring and stretching (Fig.~\ref{fig:lanemarking_illustration}). To tackle this issue, we adopt the Encoder-Decoder architecture in Fully Convolutional Networks~\cite{FCN} and leverage the idea of Spatial Transformer Networks~\cite{STN} to build a semantic segmentation neural network.
As shown in Fig.~\ref{fig:network_structure}, Fully Convolutional layers are interleaved with a series of differentiable homographic transform layers called "Perspective Transformer Layers" (PTLs) which can transform the feature maps from the original view to the bird's-eye view during the encoding process. Afterwards, it transforms feature maps back to the original perspective in the decoding process, where subsequent convolutional layers are employed to refine each interpolated feature map.
Therefore, this network can still use the labels in the original view for an end-to-end training.

In this work, our contributions can be summarized as follows:

\iffalse

\fi

\begin{itemize}
    \item We proposed a lane marking detection network based on FCN, which integrates with novel PTLs to reduce the perspective distortion at a distance.
    \item We build a mathematical model to  derive the parameters of consecutive PTLs, enabling the mutual conversion between the original view and the bird's eye view step-wisely.
    \item The effectiveness of the proposed method in both instance segmentation and semantic segmentation for lane and road markings is approved on two public datasets: TuSimple~\cite{TuSimple} and ApolloScape~\cite{apolloscape_arXiv_2018}.
\end{itemize}{}

\begin{figure*}[tbp]
    \centering
    \includegraphics[width=\textwidth]{final_Net.png}
    \caption{PTSeg architecture. Semantic segmentation network is the main body of PTSeg. It is based on a standard
    encoder-decoder network introduced in \cite{FCN}, of which the encoder is implemented with a ResNet-34 network~\cite{ResNet}. Each Perspective Transformer Layer (PTL) follows a ResBlock or a Transposed Convolution layer, perspectively and gradually warping feature maps into a bird's-eye view or back to front-view. The process of perspective transform is visualized qualitatively using color images above the main network. As for instance segmentation, following~\cite{LaneNet}, an instance embedding branch is added. It shares previous layers with the semantic segmentation networks and outputs N-dimensional embedding per lane pixel, which is also visualized as a color map.}
    \label{fig:network_structure}
\end{figure*}

\section{RELATED WORKS\label{sec:related_works}}
Lane marking detection has been intensively explored and recent progresses have mainly focused on the semantic segmentation-based and instance segmentation-based methods.
\subsection{Lane Marking Detection by Semantic Segmentation}
The work~\cite{TsinghuaRoadMarking} proposed both a road marking dataset and a segmentation network using the ResNet with Pyramid Pooling.
Lee et al\onedot~\cite{VPGNet} proposed a unified end-to-end trainable multi-task network that jointly handles lane markings detection and road markings recognition under adverse weather conditions with the guidance by a vanishing point.
Zhang et al\onedot~\cite{Zhang2019RoadMS} proposed a segmentation-by-detection method for road marking extraction, which delivers outstanding performances on cross datasets.
In this method, a lightweight network is dedicatedly designed for road marking detection. However, the segmentation is mainly based on conventional image morphological algorithms.

\subsection{Lane Marking Detection by Instance Segmentation}
Semantic segmentation is essentially just a pixel-level classification problem, it neither can distinguish different instances within the same category, nor can interpret separated parts of the same marking (dashed lines, zebra lines, \emph{etc}\onedot} \def\vs{\emph{vs}\onedot) as a unity. Therefore, researchers' attention gradually shifted to study the problem of instance segmentation.

Pan et al\onedot~\cite{SpatialCNN} proposed the Spatial CNN (SCNN), which generalizes traditional spatial convolutions to slice-wise convolutions within feature maps, thus enabling message passing between pixels across rows and columns in a layer. This is particularly suitable for linear shaped traffic lanes.
Hsu et al\onedot~\cite{Proposal-Free} proposed a novel learning objective function to train the deep neural network to perform an end-to-end image pixel clustering and applied this approach on instance segmentation.
Neven et al\onedot~\cite{LaneNet} went beyond the modeling limitation by pre-defined number of lanes, in their instance segmentation method each lane forms its own instance and the network can be trained end-to-end. They further proposed H-Net to parameterize the segmented results.

\subsection{Perspective Transform in CNNs}
To compensate the perspective distortion, a spatial transform, such as IPM, should be involved in the networks.
A typical work is the Spatial Transformer Network~\cite{STN}. It introduces a learnable module, which explicitly allows the spatial manipulation of data within the network. This differentiable module can be applied to existing convolutional architectures, enabling actively  spatial transform of feature maps.

The most similar work to ours is  \cite{Bruls2019BoostedIPM}. In this work, an adversarial learning approach is proposed for generating an improved IPM using the STN. The generated BEV images contain sharper features than that produced by traditional IPM.
The main difference between this work and ours is that they took a ground-truth BEV image (obtained by a visual odometry) for supervision. Their target is to generate a high-resolution IPM, while ours is to improve the segmentation accuracy.

\iffalse

\fi

\section{PROPOSED METHOD\label{sec:method}}
In this work, we boost the performance of lane marking detection by inserting differentiable PTLs into the standard encoder-decoder architecture. One challenge in designing Transformer layers lies in dividing and distributing the integral transform into several even steps. Another is about how to determine the proper cropping range for these intermediate views.
In this section, we firstly describe the improved backbone in section~\ref{sec:network_structure}.
Then, we address how to apply Transformer layers as well as how to solve above difficulties in section~\ref{sec:consecutive_perspective_mapping}.
Finally, we illustrate the deployment of the backbone in both semantic and instance segmentation context with details about detection heads and loss functions in~\ref{sec:loss function}.

\subsection{Network Structure\label{sec:network_structure}}
As shown in Fig.~\ref{fig:network_structure}, the overall semantic segmentation network is based on a standard encoder-decoder network~\cite{FCN}, in which the encoder is implemented with a ResNet-34 network~\cite{ResNet} and PTLs interleave with the convolutional layers. We refer our network as PTSeg (Perspective Transformer Segmentors). In this network, images are down-sampled by the encoder to a feature map with 5 times of the stride-2 down-sampling operation. And the feature map is gradually warped into a pseudo BEV. Afterwards, the decoder reverts the previous transforms by up-sampling and back-projecting the feature map into its original size and perspective, while keeping the accumulated high-level semantic information of lane and road markings. The process of perspective transform is visualized qualitatively using color images above the main network.

As the sampling procedure does not affect the overall differentiability, the network with PTL can be trained end-to-end. Feature maps in the middle section of the network have perspective transform relationships with the input image, and the effect of these transforms in encoding process is equivalent to warping the front-view feature maps to a BEV, thus solving the problem of inconsistent scales of lane and road markings due to different distances.
Meanwhile, the subsequent refinement reduces blur and artifacts caused by interpolation.
Similar to the FCN, skip-connections can compensate for the information loss during the down-sampling, resulting in clear boundaries for detected lane and road markings.

\subsection{Consecutive Perspective Mapping\label{sec:consecutive_perspective_mapping}}
In order to map the front-view image into a bird's-eye view smoothly, we adopt an approach differing from the standard IPM method. Here we decompose the integral transform $\mathbf{H}$ into a series of shortest-path consecutive transforms $\left\{\mathbf{H}_{i,i+1}\right\}$ (${\mathbf{H}_i}$ for short) that project the view $i$ into view $i+1$. This procedure is interpreted as
\begin{equation}\label{eqn:H_decomp_with_t_d}
\mathbf{H} = \prod_{i=0}^{N} \mathbf{H}_i \sim \prod_{i=0}^{N} \left[ \mathbf{K}_{i+1} \left(\mathbf{R}_{i,i+1}-\frac{\mathbf{t}_i\mathbf{n}_i^\top}{d_i}\right) \mathbf{K}_{i}^{-1} \right],
\end{equation}
where $\mathbf{R}_{i,i+1}$ (can be denoted as ${\mathbf{R}_i}$ for short) is the rotation matrix by which virtual camera $i+1$ is rotated in relation to virtual camera $i$; $\mathbf{t}_i$ is the translation vector from $i$ to $i+1$; $\mathbf{n}_i^\top$ and $d_i$ are the normal vector of the ground plane and the distance to the plane respectively. $\mathbf{K}_i$ and $\mathbf{K}_{i+1}$ are the cameras' intrinsic parameter matrices.

However, to control the transform process, the value of internal parameters, \emph{i.e}\onedot} \def\Ie{\emph{I.e}\onedot, $\mathbf{K}_i, \mathbf{R}_i, \mathbf{t}_i, $ and $d_i$ should be selected for each $\mathbf{H}_{i,i+1}$ by trial and error, which is a tedious job. To simplify this process, we use a pure rotation virtual camera model to eliminate $\mathbf{t}_i$, $d_i$, and use a Key-Point Bounding-Box Trick to estimate $\mathbf{K}_i$ for optimal viewports of intermediate feature maps (as shown in Algorithm~\ref{alg:optimal_view_ports}). Whereas the traditional IPM uses at least 4 pairs of pre-calibrated correspondences on each view to estimate the integral $\mathbf{H}$ directly, we estimate the integral rotation by the horizon line specified on the image, which can be obtained by horizon line detection models, \emph{e.g}\onedot} \def\Eg{\emph{E.g}\onedot, the HLW\cite{HLW}. By representing the rotation in the axis-angle form, it is much easier to divide the rotation $\mathbf{R}\in \mathbb{SO}_3$ into sections by dividing the angle $\|\mathbf{\omega}\| \in \mathbb{R}$ and keep the axis direction unchanged. In this way, all internal parameters of each $\mathbf{H}_{i,i+1}$ are determined. Details about above procedure are given as follows.

\subsubsection{Pure Rotation Virtual Cameras}\, It can be proven that a translated camera with unchanged intrinsic matrix can produce the same image as a fixed camera with accordingly modified intrinsic matrix. Thus, the consecutive perspective transform is modeled as synthesizing the ground plane image captured by a pure rotating camera, and (\ref{eqn:H_decomp_with_t_d}) is simplified as,

\begin{equation}\label{eqn:H_decomp}
    \mathbf{H}_i = \mathbf{K}_{i+1} \mathbf{R}_{i,i+1} \mathbf{K}_{i}^{-1},
\end{equation}
and only the rotation matrix should be decomposed as
\begin{equation}
    \mathbf{R} = \prod_{i=0}^{N} \mathbf{R}_{i,i+1}.
\end{equation}

\subsubsection{Estimating Integral Extrinsic Rotation by the Horizon Line}
As extrinsic matrices with respect to the ground plane are not provided in TuSimple and ApolloScape datasets, we roughly estimate the integral rotation by the horizon line. Given two horizon points in the camera coordinates, $\mathbf{p}_{\text{left}}$ and $\mathbf{p}_{\text{right}}$, the normal vector of ground plane (facing to the ground) is calculated by a cross-production, \emph{i.e}\onedot} \def\Ie{\emph{I.e}\onedot,
\begin{equation}
\mathbf{n}=\frac{\mathbf{p}_{\text{left}}\times\mathbf{p}_{\text{right}}}{\|\mathbf{p}_{\text{left}}\times\mathbf{p}_{\text{right}}\|}.
\end{equation}
In order to rotate the camera to face to the ground, its $z$-axis should be rotated to align with the normal vector $\mathbf{n}$. Hence, the rotation in axis-angle form is calculated as
\begin{equation}
\mathbf{\omega} = \frac{\mathbf{e}_3 \times \mathbf{n} }{\|\mathbf{e}_3 \times \mathbf{n}\|} \cdot \text{atan2}\left(\|\mathbf{e}_3 \times \mathbf{n}\|,\mathbf{e}_3 \cdot \mathbf{n}\right),
\end{equation}
where $\mathbf{e}_3 = (0, 0, 1)^\top$ is a unit vector on $z$-axis.

\subsubsection{Decomposing the Extrinsic Rotation}
Here we use the axis-angle representation for decomposing the rotation. We simply divide the integral angle into several even parts, and then convert each $\mathbf{\omega}_i$ to the corresponding rotation matrix $\mathbf{R}_i$.

\subsubsection{Optimal Viewports by Key-Point Bounding Boxes}
While conducting IPM, image pixels at the edge often need to be cropped to prevent the target view from being too large. In order to preserve the informative pixels as many as possible, we roughly annotate the ground region by a set of border points in the front-view. The points are projected to the new view during each perspective transform. And we use a bounding box in the new view to determine the minimal available viewport which does not crop any projected key point. Thus, given a desirable target view width $W_{i+1}$, the corresponding intrinsic $K_{i+1}$ and target view height $H_{i+1}$ is determined, as shown in Algorithm \ref{alg:optimal_view_ports}.

\begin{algorithm}[tbp]
    \caption{Determine the Optimal Viewports through Key-Point Bounding Boxes}\label{alg:optimal_view_ports}
    \begin{algorithmic}[1]
        \REQUIRE $\mathbf{K}_i$, $\mathbf{R}_i$, $\mathbf{p}_{i,j}^I$, $W_{i+1}$
        \STATE Convert points from Image $I$ to Camera $C$: $\mathbf{p}_{i,j}^C = \mathbf{K}_i^{-1} \mathbf{p}_{i,j}^I$
        \STATE Rotate points to view $i+1$: $\mathbf{p}_{i+1,j}^C = \mathbf{R}_i \mathbf{p}_{i,j}^C$
        \STATE Normalize by the Z-dimension: $\mathbf{p}_{i+1,j}^C /= \text{abs}\left(Z_{\mathbf{p}_{i+1,j}^C}\right)$
        \STATE Get the bounding box: [$bb_{top}, bb_{left}, bb_{width}, bb_{height}] = bbox(\mathbf{p}_{i+1,:}^C)$
        \STATE Estimate focal length $f_{i+1}$ as a scale ratio: $f_{i+1} = W_{i+1} / bb_{width}$
        \STATE Estimate target view height with the same scale ratio: $H_{i+1} = f_{i+1} \times bb_{height}$
        \STATE Estimate translation $t_{i+1}$ by aligning left-top corner of target image view and bounding box in target camera coordinate: $t_{i+1} = {(0, 0)}^\top - {(f_{i+1} \times bb_{left}, f_{i+1}\times bb_{top})}^\top$
        \STATE Compose target intrinsic matrix: $ \mathbf{K}_{i+1} = (f_{i+1}, t_{i+1}) $
        \RETURN $\mathbf{K}_{i+1}$, $H_{i+1}$
    \end{algorithmic}
\end{algorithm}

\subsection{Segmentation Heads\label{sec:loss function}}

\subsubsection{Semantic Segmentation\label{sec:semantic_segmentation_head}}

The lane and road marking detection problems are often cast as a semantic segmentation task~\cite{VPGNet}~\cite{TsinghuaRoadMarking}~\cite{Zhang2019RoadMS}. By representing label classes as one-hot vectors, we predict the logits of each class at each pixel location. Then, we use the classic cross-entropy loss function to train this semantic segmentation branch.

\subsubsection{Instance Segmentation\label{sec:instance_segmentation_head}}

We follow the work of LaneNet~\cite{LaneNet} to interpret the lane detection problem as an instance segmentation task. The network contains two branches. The semantic branch outputs a binary mask, while the instance embedding branch outputs an N-dimensional embedding vector for each pixel. In the embedding space pixels are more easily to be clustered by a one-shot method based on distance metric learning~\cite{brab2017semantic}. For details of the loss function please refer to~\cite{LaneNet}.

\section{EXPERIMENTS\label{sec:experiments}}
We evaluate our network on the TuSimple~\cite{TuSimple} and ApolloScape~\cite{apolloscape_arXiv_2018} dataset respectively for the instance segmentation and semantic segmentation tasks. Our network is implemented by the PyTorch~\cite{PyTorch} framework.

\subsection{TuSimple Benchmark}
\subsubsection{Dataset}
The TuSimple Benchmark is a dedicated dataset for lane detection and consists of 3626 training and 2782 testing images. The annotation includes the $x$-position of the lane points at a number of discretized $y$-positions.

\subsubsection{Metrics}
The detection accuracy is calculated as the average correct number of points per image:
\begin{equation}
    \mathrm{acc}=\sum_{i m} \frac{C_{i m}}{S_{i m}},
\end{equation}
where $C_{i m}$ denotes the number of correct points and $S_{i m}$ is the number of groundtruth points. A point is regarded as correctly detected when the error is smaller than a predefined threshold. Besides, the false positive and false negative scores can also be calculated by
\begin{equation}
\mathrm{FP} =\frac{F_{\text {pred}}}{N_{\text {pred}}} , ~~~
\mathrm{FN} =\frac{M_{\text {pred}}}{N_{g t}},
\end{equation}
where $F_{\text {pred}}$ denotes the number of mispredicted lanes, $N_{\text {pred}}$ indicates the number of predicted lanes, $M_{\text {pred}}$ is the number of missed groundtruth lanes and $N_{\text {gt}}$ represents the number of all groundtruth lanes.

\subsubsection{Training Details}
Here we train the instance segmentation network as shown in Fig.~\ref{fig:network_structure}. During the training process we use the Adam~\cite{kingma2014adam} optimizer, with a weight decay of 0.0005, a momentum of 0.95, a learning rate of 0.00004, and a batch size of 2. When the accuracy is without promotion up to 60 epochs, the learning rate drops to 10\%. And the model converges after 220 epochs.

 \begin{table}[tbp]
\caption{Test results on TuSimple Lane Detection Benchmark. \hspace{\textwidth} \footnotesize{ (u.h. is short for the region under the horizon line.)}}
\label{tab:tusimple_compare_with_others}
	\resizebox{0.98\linewidth}{!}{ %
		\setlength\tabcolsep{5pt}
\begin{tabular}{llllll}
\hline
                       & ACC   & FP     & FN     & Ext.data   & ACC(u.h.)\\ \hline
Xingang Pan{~\cite{SpatialCNN}}      & 96.53 & 0.0617 & 0.018  & yes  & N/A      \\
Yen-Chang Hsu{~\cite{Proposal-Free}}    & 96.50  & 0.0851 & 0.0269 & no  & N/A       \\
Davy Neven{~\cite{LaneNet}}       & 96.40  & 0.078  & 0.0244 & no  & N/A       \\ \hline
ResNet34-FCN     & 96.24 & 0.0746 & 0.0347 & no  & 95.67       \\
ResNet34-PTL-FCN (ours) & 96.15 & 0.0818 & 0.0314 & no  & 95.72       \\ \hline
\end{tabular}
}
\end{table}

\begin{figure}[tp]
    \centering
    \vspace*{-1.0cm}
    \subfigure[Lane points accuracy vs. distance in pixels.]{
        \includegraphics[width=\linewidth, trim = 0mm 0mm 0mm 12mm, clip=true]{ori_pixel.png}
    }%
    \\
    \subfigure[Lane points accuracy vs. distance in meters.]{
        \includegraphics[width=\linewidth, trim = 0mm 0mm 0mm 12mm, clip=true]{ori_meter.png}
    }%
    \caption{TuSimple Lane Detection Benchmark Results.}
    \label{fig:compare_tusimple}
\end{figure}

\begin{figure}[tp]
    \centering

    \includegraphics[width=\linewidth]{visual_Tusimple.png}
    \caption{Visualization of the comparison among the base-line, our method and the groundtruth on Tusimple dataset. Each row contains three submaps. From left to right: results w/o PTLs, results w/ PTLs, GT. And the area inside the red wireframe should be paid more attention. }
    \label{fig:Visua_Tusimple}
    \end{figure}

\subsubsection{Evaluation Results}
In comparison with other state-of-the-art methods~\cite{LaneNet}~\cite{SpatialCNN}~\cite{Proposal-Free}, we show the test results in Table~\ref{tab:tusimple_compare_with_others}, from which we can find out that our detection accuracy is already in the first echelon.
It is worth to mention that all evaluation results above are in strict accordance with the metric defined by TuSimple. However, in our method the feature maps are warped into a bird's-eye view of the ground, which force a part of the image above the horizon to be ignored by our method. An amount of lane segments existing above the horizon are visible for other methods but invisible for our method, which would lead to a slight decrease of the results. In order to make a fair comparison, we re-evaluated those samples only below the horizon, and ignored null sample points which is labeled as $-2$ in the annotation\footnote{See the labeling protocol in TuSimple.}. The new evaluation result is listed in $ACC(under horizon)$ column of Table~\ref{tab:tusimple_compare_with_others}. We also plot the accuracy versus different distances from ego-vehicle in the line charts.
Fig.~\ref{fig:compare_tusimple}~(a) shows the accuracy in dependence of pixel distance to the image bottom. Fig.~\ref{fig:compare_tusimple}~(b) shows the accuracy in dependence of the real distance to the ego-vehicle. Both charts imply that our method can improve the detection accuracy of lane and road markings at longer distances.
The qualitative comparison is shown in Fig.~\ref{fig:Visua_Tusimple}.

\subsection{ApolloScape Benchmark}
\subsubsection{Dataset}
The Lane Segmentation branch in ApolloScape dataset contains more than 110,000 frames with high quality pixel-level annotations. The annotation includes 35 kinds of lane and road markings from daily traffic scenarios, including but not limited to lanes, turning arrows, stop lines, zebra crossings.
To the best of the authors' knowledge, no related works have been trained on the ApolloScape Lane Segmentation dataset. Therefore, we only show the ablation experimental results of our own method.

\subsubsection{Metrics}
The evaluation follows the recommendation of ApolloScape which uses the mean-IOU (mIOU) as the evaluation metric just like in~\cite{Cordts2016Cityscapes}.

\begin{figure}[tbp]
    \centering
    \vspace*{0.0cm}
    \subfigure[mean-IOU vs. distance in pixels]{
        \includegraphics[width=\linewidth, trim = 0mm 0mm 0mm 12mm, clip=true]{split_miou_result_pixel.png}
    }%
    \\
    \subfigure[mean-IOU vs. distance in meters]{
        \includegraphics[width=\linewidth, trim = 0mm 0mm 0mm 12mm, clip=true]{split_miou_result_distance.png}
    }%
    \caption{Apollo Road Marking Semantic Segmentation Results.}
    \label{fig:compare_apollo}
\end{figure}

\subsubsection{Training Details}
Since the ApolloScape only provides pixel-level semantic annotations, we train the semantic segmentation network as shown in Fig.~\ref{fig:network_structure}.
During the training process we use the Adam~\cite{kingma2014adam} optimizer, with a weight decay of 0.0005, a momentum of 0.95, a learning rate of 0.00004, and a batch size of 2. And the model converges after 25 epochs.

\subsubsection{Evaluation Results}
Also in a fair way, we evaluate the image part below the horizon. Fig.~\ref{fig:compare_apollo} shows the results of mean-IOU accuracy at different distances.
Table~\ref{tab:apollo_per_class_iou} shows mIOU value and IOU values of some common types of lane and road markings. We ignored the rest classes who accounting for less than 0.1\% of the data.

\begin{table}[tbp]
\caption{Per-class IOU results on ApolloScapes Lane Segmentation Benchmark.}
\label{tab:apollo_per_class_iou}
	\resizebox{0.98\linewidth}{!}{ %
		\setlength\tabcolsep{5pt}
\begin{tabular}{llcc}
\hline
category                   & class               & ResNet18-FCN      & ResNet18-PTL-FCN (ours)  \\ \hline
\multirow{4}{*}{arrow} & thru                & 0.611          & \textbf{0.692} \\
                       & thru \& left turn   & 0.768          & \textbf{0.800}  \\
                       & thru \& right turn  & \textbf{0.824} & 0.808          \\
                       & left turn           & 0.767          & \textbf{0.768} \\ \hline
stopping               & stop line           & 0.665          & \textbf{0.747} \\ \hline
zebra                  & crosswalk           & \textbf{0.859}  & 0.858           \\ \hline
\multirow{4}{*}{lane}  & white solid         & \textbf{0.832} & 0.800          \\
                       & yellow solid        & \textbf{0.813} & 0.803          \\
                       & yellow double solid & 0.886          & \textbf{0.893} \\
                       & white broken        & \textbf{0.791} & 0.790          \\ \hline
diamond                & zebra attention     & 0.749          & \textbf{0.775} \\ \hline
rectangle              & no parking          & 0.652           & \textbf{0.724} \\ \hline
mIOU              &            & 0.768           & \textbf{0.788} \\ \hline
\end{tabular}
}
\end{table}

According to the experimental results, our method can effectively improve the detection accuracy at further distances, especially for the road markings with richer structural features such as turning arrows.
The qualitative comparison is shown in Fig.~\ref{fig:Visua_Apollo}.

\begin{figure}[tbp]
    \centering
    \includegraphics[width=\linewidth]{visual_Apollo2.png}
    \caption{Visualization of the comparison among the base-line, our method and the ground-truth on ApolloScape. Each row contains three submaps. From left to right: results w/o PTLs, results w/ PTLs, GT, and the enlarged view of area inside the red wireframe is placed on the top of each submap.}
    \label{fig:Visua_Apollo}
    \end{figure}

\section{CONCLUSION\label{sec:conclusion}}
In this paper, we introduced a segmentation network architecture improved by consecutive homography transforms for road marking detection. The parameters of consecutive transforms are clearly yielded by a pure rotating camera model and a key-point bounding-box trick. The proposed method is proven to be beneficial for distant lane and road marking detection.
For the future research, we are going to incorporate an online scheme of extrinsic estimation into this structure. Also handling the non-flat ground surface which has unclear definition of ground normal vectors and horizon lines is one of the interesting topics.

\section*{Acknowledgment}
This work is supported by the National Key Research and Development Program of China (No. 2018YFB0105103, No. 2017YFA0603104), the National Natural Science Foundation of China (No. U1764261, No. 41801335, No. 41871370), the Natural Science Foundation of Shanghai (No. kz170020173571, No. 16DZ1100701) and the Fundamental Research Funds for the Central Universities (No. 22120180095).

\bibliographystyle{unsrt}