Date: Fri, 16 Oct 2015 10:48:51 +0100 From: Hannes Mehnert <hannes@mehnert.org> To: freebsd-transport@freebsd.org Subject: Re: Documents from Peter Sewell on TCP stack... Message-ID: <5620C803.60501@mehnert.org> In-Reply-To: <CAHWkzRRjzxn=P1xKRkGig3jYkLxd4o6wG1KHMd65%2BcwFs4gT3A@mail.gmail.com> References: <F69FFAB6-036D-4804-B9BB-EFFF8F1DC607@neville-neil.com> <CAHWkzRTrsf3N%2BXo7F6Rg6DXkZHeGQTFHw_nLyK5BhHhfVKYQjw@mail.gmail.com> <20151014165820.GM87252@strugglingcoder.info> <CAHWkzRRjzxn=P1xKRkGig3jYkLxd4o6wG1KHMd65%2BcwFs4gT3A@mail.gmail.com>
next in thread | previous in thread | raw e-mail | index | archive | help
This is an OpenPGP/MIME signed message (RFC 4880 and 3156) --UswfklP0F98KhklmbB8hvU53HUSFJt9gG Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable 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@strugglingcoder.in= fo> > 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, orien= ted > towards testing connection setup, teardown, and suchlike, rather than l= ong > 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 fast= er - 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 outp= ut) - 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/auto= test [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/auto= test/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=3D203467 --UswfklP0F98KhklmbB8hvU53HUSFJt9gG Content-Type: application/pgp-signature; name="signature.asc" Content-Description: OpenPGP digital signature Content-Disposition: attachment; filename="signature.asc" -----BEGIN PGP SIGNATURE----- Version: GnuPG v2 iQIcBAEBCQAGBQJWIMgIAAoJELyJZYjffCjuTccQAJ/0/dlfWtL2/VxbMPtybT9W tU2J1xfMEwnq3ujmvFlJG4lB3TqGDPGU0c+8awg6xK+rHYN19vZNRpLqeGB2KrbA adkyuKLn3ftdgdBirBKtvDC7tXH3wYKWzCitUY3559hdeJMSReuypxMzscuEBqB0 16ocnMRC4699SNFA5H0Ev591azHOvg2178AiNP+zq6Rdir1eZCS6h0lLDxy88Tho 5WWKHStEeTiihtM42sQrEi6i5QQxlhDLklvzHauey0vx+Sga6jyEOLeTTbE2RJEW hvq43PxOk4QK3mXzbhJ6/vHsR9EysZoI/KD1KSd1XwScWgfPogkJd5RiNQzqAgvp 6RG/qPiFsrrXqLHZef3pf56+zXT1wm3Ixf5kfJCXvH8y+h8HhGuZCxpQXJv/Axel CYT8j50ekNx/BpCK9QiCP/+3pEoCcobginEpIfuPZJYvf8BiAedQvZkWM0hJ7Div u+tECmwI2vmUDrg8mz1iVWLCjOJxTaBe5LgDdM8lUYrz049aEGreg6V1hU1k1iby viOGGbb3i9fsv96x1EVoC+HJFSIIDxytQc+WNIlX44PTF+7vswSep9rXsgQrB1vd A+8SCfLzICBguPtMbMSbHWwPLrsppHYxSOZaFAOKr+kZrlJpupF0LmyKMxaWzpmz n9lsZ0uDwNY2TLIqdthn =qQmb -----END PGP SIGNATURE----- --UswfklP0F98KhklmbB8hvU53HUSFJt9gG--
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?5620C803.60501>