Documents from Peter Sewell on TCP stack...

[Hannes Mehnert]

Hi,

sorry for the delayed reply.  Questions are answered out of order.

Let me briefly introduce myself: I use FreeBSD since 4.5 (stable on my
server; CURRENT on my workstation), I did a PhD in formal verification
of imperative programs; and am currently working as a postdoc in Peter's
research group [-2].  I am interested in robust and rigorous engineering
of widely used systems [-1].

I haven't been involved with the original project (still conducting
archaeology of the artifacts).  Also, several of the original authors
are supportive (answering questions and contributing code).


On 10/14/2015 18:07, Peter Sewell wrote:
> On 14 October 2015 at 17:58, hiren panchasara <hiren at strugglingcoder.info>
> wrote:
>> 2) How many total test-cases have you created for TCP? Section 5.
>> RESULTS mentions 1095 total traces and 1004 turned out good bases on
>> the test-cases. Where do I look at the test-cases in detail?
>>
>
> There's more detail about the test generation in Section 3 of "Volume 1".
> We generated around 1000 TCP tests - they're mostly pretty short, oriented
> towards testing connection setup, teardown, and suchlike, rather than long
> connections that move significant data.  I don't think we put the
> individual traces on the web anywhere, but perhaps Hannes can send you a
> few.


The test framework [0] is written in OCaml.  It compiles, but I haven't
gotten around to re-run it yet.

A simple trace (trace [1], pdf version [2], test source [3]) creates a
socket and `connect`s to a loopback address and port (and fails).  A
more complex trace (trace [4], pdf version [5], source missing)
successfully establishes a connection and sends some data over it before
closing.

The tests contain of
 - calls to the sockets API for the system under test
 - possibly another host, which runs some listening service and/or
injects raw TCP frames

A trace consists of events, which are
 - calls to the sockets API (and return values)
 - packets on the wire
 - TCP control block dumps (using the TCPDEBUG kernel option)
 - time passed (Lh_epsilon)

These events are collected by various programs, and then merged into a
single trace (depending on timestamps to get them into linear order).


Current state:
 - We have ~2000 traces, and of those ~1000 results from 10 years ago.
 - The project has been ported from HOL4 from 2005 to a current version
(see [6], including port to PolyML [7])

Next steps:
 - Validate that the trace checker from today works (similar to the one
from 10 years ago) [in progress]
   - initial results (~50% done) look promising, roughly 10-20 times faster
 - Gather new traces from a FreeBSD-CURRENT (likely switching off the
TCP features the model does not support, such as SACK/ECN)
 - Switch to use dtrace instead of TCPDEBUG (more fine grained, more output)
 - Avoid backtracking in the model by getting more tracing
 - Do tracing and trace checking on multiple platforms
(FreeBSD/Linux/MacOS?)
 - Extend the model with missing TCP features
 - Deal with congestion control (tests with multiple connections)
 - A more rigorous test suite (if we can come up with any)


This is roughly the roadmap (or at least my tentative); timeframe is
"working on it",

hannes

[-2]: https://rems.io
[-1]: https://nqsb.io
[0]:
https://github.com/PeterSewell/netsem/tree/master/Net/TCP/Test/tests/autotest
[1]: http://www.cl.cam.ac.uk/~hm519/traces/trace0002.epsilon
[2]: http://www.cl.cam.ac.uk/~hm519/traces/trace0002.pdf
[3]:
https://github.com/PeterSewell/netsem/blob/master/Net/TCP/Test/tests/autotest/loopback.ml
[4]: http://www.cl.cam.ac.uk/~hm519/traces/trace0875.epsilon
[5]: http://www.cl.cam.ac.uk/~hm519/traces/trace0875.pdf
[6]: https://github.com/PeterSewell/netsem/
[7]: https://bugs.freebsd.org/bugzilla/show_bug.cgi?id=203467

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://lists.freebsd.org/pipermail/freebsd-transport/attachments/20151016/acb06ece/attachment.bin>