Documents from Peter Sewell on TCP stack...
hannes at mehnert.org
Fri Oct 16 09:49:42 UTC 2015
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>
>> 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
The test framework  is written in OCaml. It compiles, but I haven't
gotten around to re-run it yet.
A simple trace (trace , pdf version , test source ) creates a
socket and `connect`s to a loopback address and port (and fails). A
more complex trace (trace , pdf version , source missing)
successfully establishes a connection and sends some data over it before
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).
- 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 , including port to PolyML )
- 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
- 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",
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 819 bytes
Desc: OpenPGP digital signature
More information about the freebsd-transport