From owner-freebsd-transport@freebsd.org Mon Oct 12 17:19:29 2015 Return-Path: Delivered-To: freebsd-transport@mailman.ysv.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2001:1900:2254:206a::19:1]) by mailman.ysv.freebsd.org (Postfix) with ESMTP id 98294A118A3 for ; Mon, 12 Oct 2015 17:19:29 +0000 (UTC) (envelope-from hiren@strugglingcoder.info) Received: from mailman.ysv.freebsd.org (mailman.ysv.freebsd.org [IPv6:2001:1900:2254:206a::50:5]) by mx1.freebsd.org (Postfix) with ESMTP id 7FDF3B8 for ; Mon, 12 Oct 2015 17:19:29 +0000 (UTC) (envelope-from hiren@strugglingcoder.info) Received: by mailman.ysv.freebsd.org (Postfix) id 7D93BA118A2; Mon, 12 Oct 2015 17:19:29 +0000 (UTC) Delivered-To: transport@mailman.ysv.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2001:1900:2254:206a::19:1]) by mailman.ysv.freebsd.org (Postfix) with ESMTP id 7C385A118A1 for ; Mon, 12 Oct 2015 17:19:29 +0000 (UTC) (envelope-from hiren@strugglingcoder.info) Received: from mail.strugglingcoder.info (strugglingcoder.info [65.19.130.35]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client CN "mail.strugglingcoder.info", Issuer "mail.strugglingcoder.info" (not verified)) by mx1.freebsd.org (Postfix) with ESMTPS id 62CE2B7 for ; Mon, 12 Oct 2015 17:19:29 +0000 (UTC) (envelope-from hiren@strugglingcoder.info) Received: from localhost (unknown [10.1.1.3]) (Authenticated sender: hiren@strugglingcoder.info) by mail.strugglingcoder.info (Postfix) with ESMTPA id EF878D4761 for ; Mon, 12 Oct 2015 10:19:27 -0700 (PDT) Date: Mon, 12 Oct 2015 10:19:27 -0700 From: hiren panchasara To: transport@FreeBSD.org Subject: Re: Setting congestion window on loss detection Message-ID: <20151012171927.GB92230@strugglingcoder.info> References: <20151007195445.GC42742@strugglingcoder.info> MIME-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha512; protocol="application/pgp-signature"; boundary="Fba/0zbH8Xs+Fj9o" Content-Disposition: inline In-Reply-To: <20151007195445.GC42742@strugglingcoder.info> User-Agent: Mutt/1.5.23 (2014-03-12) X-BeenThere: freebsd-transport@freebsd.org X-Mailman-Version: 2.1.20 Precedence: list List-Id: Discussions of transport level network protocols in FreeBSD List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Mon, 12 Oct 2015 17:19:29 -0000 --Fba/0zbH8Xs+Fj9o Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Content-Transfer-Encoding: quoted-printable On 10/07/15 at 12:54P, hiren panchasara wrote: > Found this issue about a month ago and started a discussion on -net: > https://lists.freebsd.org/pipermail/freebsd-net/2015-September/043249.html >=20 > I feel this forum is a better place to discuss this further now. >=20 > Problem: We set cwnd to 1mss when we detect loss via arrivals of 3 dupack= s. > That is wrong as we severely underutilizing network capacity by doing > so. >=20 > Next question is, what should we set cwnd to? >=20 > RFC6675 (TCP SACK) suggests following on detecting loss: > ssthresh =3D cwnd =3D (FlightSize / 2) >=20 > RFC5681 (TCP Congestion control) suggest: > ssthresh =3D max (FlightSize / 2, 2*SMSS) > cwnd =3D (ssthresh + 3*SMSS) >=20 > (Here, FlightSize is bytes in flight.) >=20 > OR should we let whatever congestion control (CC) algo in control decide > that value? I also tried to look at what Linux does. It has PRR (Proportional Rate Reduction) RFC 6937 (something I plan to work on after these initial needed fixes/improvements) in place. Looking back pre-PRR code, linux seems to be doing following: cwnd =3D min(cwnd, FlightSize) Here, cwnd in the equation is adjusted as per rate-halving (draft-mathis-tcp-ratehalving-00) which says "the window is reduced by sending one data segment for each two segments which are acknowledged". (I am not very familiar with linux code so please correct me if that's not the case.) Basically, I think any of these approaches is better than what we have in the tree right now. Cheers, Hiren --Fba/0zbH8Xs+Fj9o Content-Type: application/pgp-signature -----BEGIN PGP SIGNATURE----- Version: GnuPG v2 iQF8BAABCgBmBQJWG+ucXxSAAAAAAC4AKGlzc3Vlci1mcHJAbm90YXRpb25zLm9w ZW5wZ3AuZmlmdGhob3JzZW1hbi5uZXRBNEUyMEZBMUQ4Nzg4RjNGMTdFNjZGMDI4 QjkyNTBFMTU2M0VERkU1AAoJEIuSUOFWPt/lF/AH/35US0f2QyjOIvJFR/32gjGG d63SvM0t+jE9qcDQ4VlS7nPAfIVVs/noJfOk4EP1aJGnIpLSsok03iME+hoHHRX3 gJQY6AL956buoViFwdmlETXxznpbFHYnKofcEr14InrorjM6QJxv8ddezsapk8oa ggwS+ytRqV813x8PotZ88zJk1X8k9KtE6Quy3Rf0SIz6u60yHPg2mcAQjNo/3I6r srAboh42pbP/MMn35IPY8b/046n7ZhtPOEBgau1COyztAzWiKoe/4Bxj+jWF+iae 9NALXqEM5mbJTDfw+iTEA9DJ7ncqkJg3MOSBTG22Gq7aiHuiLY2eQlVcrwhWr/U= =J3iC -----END PGP SIGNATURE----- --Fba/0zbH8Xs+Fj9o-- From owner-freebsd-transport@freebsd.org Wed Oct 14 16:58:22 2015 Return-Path: Delivered-To: freebsd-transport@mailman.ysv.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2001:1900:2254:206a::19:1]) by mailman.ysv.freebsd.org (Postfix) with ESMTP id B29ECA13AEC for ; Wed, 14 Oct 2015 16:58:22 +0000 (UTC) (envelope-from hiren@strugglingcoder.info) Received: from mailman.ysv.freebsd.org (mailman.ysv.freebsd.org [IPv6:2001:1900:2254:206a::50:5]) by mx1.freebsd.org (Postfix) with ESMTP id 9925C9D2 for ; Wed, 14 Oct 2015 16:58:22 +0000 (UTC) (envelope-from hiren@strugglingcoder.info) Received: by mailman.ysv.freebsd.org (Postfix) id 98350A13AEB; Wed, 14 Oct 2015 16:58:22 +0000 (UTC) Delivered-To: transport@mailman.ysv.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2001:1900:2254:206a::19:1]) by mailman.ysv.freebsd.org (Postfix) with ESMTP id 97C89A13AE9 for ; Wed, 14 Oct 2015 16:58:22 +0000 (UTC) (envelope-from hiren@strugglingcoder.info) Received: from mail.strugglingcoder.info (strugglingcoder.info [65.19.130.35]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client CN "mail.strugglingcoder.info", Issuer "mail.strugglingcoder.info" (not verified)) by mx1.freebsd.org (Postfix) with ESMTPS id 841309D1 for ; Wed, 14 Oct 2015 16:58:22 +0000 (UTC) (envelope-from hiren@strugglingcoder.info) Received: from localhost (unknown [10.1.1.3]) (Authenticated sender: hiren@strugglingcoder.info) by mail.strugglingcoder.info (Postfix) with ESMTPA id EA42FC34AD; Wed, 14 Oct 2015 09:58:20 -0700 (PDT) Date: Wed, 14 Oct 2015 09:58:20 -0700 From: hiren panchasara To: Peter Sewell Cc: George Neville-Neil , transport@freebsd.org Subject: Re: Documents from Peter Sewell on TCP stack... Message-ID: <20151014165820.GM87252@strugglingcoder.info> References: MIME-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha512; protocol="application/pgp-signature"; boundary="JLiXfqD9/Kt1b+Pq" Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.23 (2014-03-12) X-BeenThere: freebsd-transport@freebsd.org X-Mailman-Version: 2.1.20 Precedence: list List-Id: Discussions of transport level network protocols in FreeBSD List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 14 Oct 2015 16:58:22 -0000 --JLiXfqD9/Kt1b+Pq Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Content-Transfer-Encoding: quoted-printable On 10/10/15 at 04:30P, Peter Sewell wrote: > On 10 October 2015 at 16:27, George Neville-Neil > wrote: >=20 > > Howdy, > > > > These are a bit long but this is the work that Peter (who I think is now > > on this list) and his group > > did in 2005 on the FreeBSD TCP stack. > > > > http://www.cl.cam.ac.uk/~pes20/Netsem/tr.pdf > > http://www.cl.cam.ac.uk/~pes20/Netsem/alldoc.pdf > > > > Much of the overview material including the "Quick Introduction" which I > > recommend you read first, > > is here http://www.cl.cam.ac.uk/~pes20/Netsem/index.html Thanks George. > > > > > (probably the SIGCOMM paper [http://www.cl.cam.ac.uk/~pes20/Netsem/paper.= ps] > comes after that) Thanks Peter for the link. I (very) briefly looked at it and have a few questions (apologies if I missed something obvious): 1) It refers to FreeBSD 4.6-R. Have you tried any newer version? 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? 3) Section 6. IMPLEMENTATION ANOMALIES lists a bunch of bugs. It'd be good to know if they are now fixed or not. I think this is a great piece of work. I'd be interested in knowing future plans wrt this project. Cheers, Hiren --JLiXfqD9/Kt1b+Pq Content-Type: application/pgp-signature -----BEGIN PGP SIGNATURE----- Version: GnuPG v2 iQF8BAABCgBmBQJWHompXxSAAAAAAC4AKGlzc3Vlci1mcHJAbm90YXRpb25zLm9w ZW5wZ3AuZmlmdGhob3JzZW1hbi5uZXRBNEUyMEZBMUQ4Nzg4RjNGMTdFNjZGMDI4 QjkyNTBFMTU2M0VERkU1AAoJEIuSUOFWPt/lC3YIAIG/oUvsTY5NVKbVIVs8d/aD hkNfgiLw7Ngm6DDwEfRMTIC6H/L7g2AluErCEBNsRTkmn9BxeSvDnwqdFPJi9UKb Ju+AUYSyW2VgjduKKO7A2A6y65ZcFtuFz4n3YYedHFN58l/kJydDBIJkUMarnTto DMRcdU4uEZ2x2LqgJpbnHH4i31aTPvgBaLGKJdWvacp9IMsc+TbhqSwoEoEBsVK/ 5vDMPHQhWIxgQhDmPZZg6JtU6yE7x8le4U036YygVnnVrjyQFRb3x0qo03CbGrBO HB1NFfJKdd+VPQ2aSluSyd3kyT+R4gfgT4IIOcNMGmHrHL6tagvjSBSh2M+AZ3c= =b0Fw -----END PGP SIGNATURE----- --JLiXfqD9/Kt1b+Pq-- From owner-freebsd-transport@freebsd.org Wed Oct 14 17:08:00 2015 Return-Path: Delivered-To: freebsd-transport@mailman.ysv.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2001:1900:2254:206a::19:1]) by mailman.ysv.freebsd.org (Postfix) with ESMTP id 8499FA142AB for ; Wed, 14 Oct 2015 17:08:00 +0000 (UTC) (envelope-from p.m.sewell@googlemail.com) Received: from mailman.ysv.freebsd.org (mailman.ysv.freebsd.org [IPv6:2001:1900:2254:206a::50:5]) by mx1.freebsd.org (Postfix) with ESMTP id 612B310E2 for ; Wed, 14 Oct 2015 17:08:00 +0000 (UTC) (envelope-from p.m.sewell@googlemail.com) Received: by mailman.ysv.freebsd.org (Postfix) id 604C9A142AA; Wed, 14 Oct 2015 17:08:00 +0000 (UTC) Delivered-To: transport@mailman.ysv.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2001:1900:2254:206a::19:1]) by mailman.ysv.freebsd.org (Postfix) with ESMTP id 5FD55A142A9 for ; Wed, 14 Oct 2015 17:08:00 +0000 (UTC) (envelope-from p.m.sewell@googlemail.com) Received: from mail-ig0-x233.google.com (mail-ig0-x233.google.com [IPv6:2607:f8b0:4001:c05::233]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (Client CN "smtp.gmail.com", Issuer "Google Internet Authority G2" (verified OK)) by mx1.freebsd.org (Postfix) with ESMTPS id 3974110E1 for ; Wed, 14 Oct 2015 17:08:00 +0000 (UTC) (envelope-from p.m.sewell@googlemail.com) Received: by igsu6 with SMTP id u6so21689226igs.1 for ; Wed, 14 Oct 2015 10:07:59 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlemail.com; s=20120113; h=mime-version:reply-to:sender:in-reply-to:references:date:message-id :subject:from:to:cc:content-type; bh=R84+Arb+MvnnFkhChkqdS+UiiTx15/+bC8SW2YdCCiw=; b=L5cYExjGBd9aWjlNrhgIwvBVi9uLh0DQ8fMjnkHhRkKGvV9ygKKILJCz9JbmT2prTT dxfftVnsdKL46EuQlD3zYVWzi7sFTMReHUibW4UtsEcoDUTj2/fZNtpmiRhBs13RP7n+ 1ELpMSHR0UawdmZIfU63ltZOk+6AyPTE1Cyzfhb4Re/Pf6XLIyr5T4GctkIPMpb8hjW5 CkmVFHM/HJgv5lbCtISu9KGO/oQJxQAlu1ao02eYeVOkb/ji4jGEmIlqhSV7lbTgwcA/ NzVFDG0LIHXWJKMU4QhiPBiX6tuYuuvGiOSeVSxshsP2nDvbGNsv+05nqHvhnoOGNXkq rWoA== MIME-Version: 1.0 X-Received: by 10.50.43.170 with SMTP id x10mr5443334igl.12.1444842479340; Wed, 14 Oct 2015 10:07:59 -0700 (PDT) Reply-To: Peter.Sewell@cl.cam.ac.uk Sender: p.m.sewell@googlemail.com Received: by 10.64.251.130 with HTTP; Wed, 14 Oct 2015 10:07:59 -0700 (PDT) In-Reply-To: <20151014165820.GM87252@strugglingcoder.info> References: <20151014165820.GM87252@strugglingcoder.info> Date: Wed, 14 Oct 2015 18:07:59 +0100 X-Google-Sender-Auth: g_GWKVNnh-Kq2qxE36SrsutFVwM Message-ID: Subject: Re: Documents from Peter Sewell on TCP stack... From: Peter Sewell To: hiren panchasara Cc: George Neville-Neil , transport@freebsd.org Content-Type: text/plain; charset=UTF-8 X-Content-Filtered-By: Mailman/MimeDel 2.1.20 X-BeenThere: freebsd-transport@freebsd.org X-Mailman-Version: 2.1.20 Precedence: list List-Id: Discussions of transport level network protocols in FreeBSD List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 14 Oct 2015 17:08:00 -0000 On 14 October 2015 at 17:58, hiren panchasara wrote: > On 10/10/15 at 04:30P, Peter Sewell wrote: > > On 10 October 2015 at 16:27, George Neville-Neil > > wrote: > > > > > Howdy, > > > > > > These are a bit long but this is the work that Peter (who I think is > now > > > on this list) and his group > > > did in 2005 on the FreeBSD TCP stack. > > > > > > http://www.cl.cam.ac.uk/~pes20/Netsem/tr.pdf > > > http://www.cl.cam.ac.uk/~pes20/Netsem/alldoc.pdf > > > > > > Much of the overview material including the "Quick Introduction" which > I > > > recommend you read first, > > > is here http://www.cl.cam.ac.uk/~pes20/Netsem/index.html > > Thanks George. > > > > > > > > (probably the SIGCOMM paper [ > http://www.cl.cam.ac.uk/~pes20/Netsem/paper.ps] > > comes after that) > > Thanks Peter for the link. I (very) briefly looked at it and have a few > questions (apologies if I missed something obvious): > These are mostly questions for Hannes and David, who have picked the project up again. > 1) It refers to FreeBSD 4.6-R. Have you tried any newer version? > Not yet, though that's part of their plan. > 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. > 3) Section 6. IMPLEMENTATION ANOMALIES lists a bunch of bugs. It'd be > good to know if they are now fixed or not. > These are also detailed in "Volume 1". We didn't chase them at the time, as we ran out of available effort - I don't recall whether we reported them. So they may or may not have been fixed. best, Peter > I think this is a great piece of work. I'd be interested in knowing > future plans wrt this project. > > Cheers, > Hiren > From owner-freebsd-transport@freebsd.org Thu Oct 15 21:02:38 2015 Return-Path: Delivered-To: freebsd-transport@mailman.ysv.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2001:1900:2254:206a::19:1]) by mailman.ysv.freebsd.org (Postfix) with ESMTP id AD65EA16103 for ; Thu, 15 Oct 2015 21:02:38 +0000 (UTC) (envelope-from gnn@neville-neil.com) Received: from mailman.ysv.freebsd.org (mailman.ysv.freebsd.org [IPv6:2001:1900:2254:206a::50:5]) by mx1.freebsd.org (Postfix) with ESMTP id 943FBF48 for ; Thu, 15 Oct 2015 21:02:38 +0000 (UTC) (envelope-from gnn@neville-neil.com) Received: by mailman.ysv.freebsd.org (Postfix) id 938BBA16102; Thu, 15 Oct 2015 21:02:38 +0000 (UTC) Delivered-To: transport@mailman.ysv.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2001:1900:2254:206a::19:1]) by mailman.ysv.freebsd.org (Postfix) with ESMTP id 93271A16101 for ; Thu, 15 Oct 2015 21:02:38 +0000 (UTC) (envelope-from gnn@neville-neil.com) Received: from smtp.hungerhost.com (smtp.hungerhost.com [216.38.53.177]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by mx1.freebsd.org (Postfix) with ESMTPS id 70A92F47 for ; Thu, 15 Oct 2015 21:02:38 +0000 (UTC) (envelope-from gnn@neville-neil.com) Received: from cpe-69-203-112-190.nyc.res.rr.com ([69.203.112.190]:51000 helo=[192.168.64.1]) by vps.hungerhost.com with esmtpsa (TLSv1:DHE-RSA-AES256-SHA:256) (Exim 4.86) (envelope-from ) id 1ZmpfZ-00075I-4K for transport@freebsd.org; Thu, 15 Oct 2015 17:02:37 -0400 From: "George Neville-Neil" To: transport@freebsd.org Subject: Phabricator group Date: Thu, 15 Oct 2015 17:02:36 -0400 Message-ID: <3EB50947-363E-4A7E-84C0-79EB756BC02B@neville-neil.com> MIME-Version: 1.0 Content-Type: text/plain; format=flowed X-Mailer: MailMate (1.9.2r5141) X-AntiAbuse: This header was added to track abuse, please include it with any abuse report X-AntiAbuse: Primary Hostname - vps.hungerhost.com X-AntiAbuse: Original Domain - freebsd.org X-AntiAbuse: Originator/Caller UID/GID - [47 12] / [47 12] X-AntiAbuse: Sender Address Domain - neville-neil.com X-Get-Message-Sender-Via: vps.hungerhost.com: authenticated_id: gnn@neville-neil.com X-Authenticated-Sender: vps.hungerhost.com: gnn@neville-neil.com X-Source: X-Source-Args: X-Source-Dir: X-BeenThere: freebsd-transport@freebsd.org X-Mailman-Version: 2.1.20 Precedence: list List-Id: Discussions of transport level network protocols in FreeBSD List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Thu, 15 Oct 2015 21:02:38 -0000 I added a few folks off the top of my head. If you're not on here but want to be please add yourself. If you can't email me off list and I'll deal with it. https://reviews.freebsd.org/project/members/62/ Best, George From owner-freebsd-transport@freebsd.org Fri Oct 16 09:49:42 2015 Return-Path: Delivered-To: freebsd-transport@mailman.ysv.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2001:1900:2254:206a::19:1]) by mailman.ysv.freebsd.org (Postfix) with ESMTP id 05B8F9D2525 for ; Fri, 16 Oct 2015 09:49:42 +0000 (UTC) (envelope-from hannes@mehnert.org) Received: from mail.mehnert.org (mail.mehnert.org [213.73.89.200]) (using TLSv1 with cipher DHE-RSA-CAMELLIA256-SHA (256/256 bits)) (Client did not present a certificate) by mx1.freebsd.org (Postfix) with ESMTPS id B818F1386 for ; Fri, 16 Oct 2015 09:49:41 +0000 (UTC) (envelope-from hannes@mehnert.org) Received: from [192.168.0.11] (cpc30-cmbg15-2-0-cust247.5-4.cable.virginm.net [86.4.51.248]) (using TLSv1 with cipher DHE-RSA-AES128-SHA (128/128 bits)) (Client CN "hannes@mehnert.org", Issuer "mehnert root CA" (not verified)) by mail.mehnert.org (Postfix) with ESMTPS id 9B2ED1F2B for ; Fri, 16 Oct 2015 11:49:32 +0200 (CEST) Subject: Re: Documents from Peter Sewell on TCP stack... To: freebsd-transport@freebsd.org References: <20151014165820.GM87252@strugglingcoder.info> From: Hannes Mehnert Openpgp: id=11B5464249B5BD858FFF6328BC896588DF7C28EE X-Enigmail-Draft-Status: N1110 Message-ID: <5620C803.60501@mehnert.org> Date: Fri, 16 Oct 2015 10:48:51 +0100 User-Agent: Mozilla/5.0 (X11; FreeBSD amd64; rv:38.0) Gecko/20100101 Thunderbird/38.3.0 MIME-Version: 1.0 In-Reply-To: Content-Type: multipart/signed; micalg=pgp-sha384; protocol="application/pgp-signature"; boundary="UswfklP0F98KhklmbB8hvU53HUSFJt9gG" X-BeenThere: freebsd-transport@freebsd.org X-Mailman-Version: 2.1.20 Precedence: list List-Id: Discussions of transport level network protocols in FreeBSD List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Fri, 16 Oct 2015 09:49:42 -0000 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 > 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--