From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 2E5B0BB84 for ; Wed, 21 May 2008 09:52:47 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AjgBALxxM0jAXQIniGdsb2JhbACSNgEBAQ8gnSw X-IronPort-AV: E=Sophos;i="4.27,519,1204498800"; d="scan'208";a="12857300" Received: from concorde.inria.fr ([192.93.2.39]) by mail3-smtp-sop.national.inria.fr with ESMTP; 21 May 2008 09:52:46 +0200 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id m4L7qgOt024623 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Wed, 21 May 2008 09:52:46 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AlIBALxxM0iKJV+LgWdsb2JhbACSNgEBECAFnSc X-IronPort-AV: E=Sophos;i="4.27,519,1204498800"; d="scan'208";a="26448175" Received: from tart.dcs.qmul.ac.uk (HELO mail.dcs.qmul.ac.uk) ([138.37.95.139]) by mail4-smtp-sop.national.inria.fr with ESMTP; 21 May 2008 09:52:46 +0200 Received: from new8-pc.dcs.qmul.ac.uk ([138.37.88.113]) by mail.dcs.qmul.ac.uk with esmtpsa (TLSv1:DHE-RSA-AES256-SHA:256) (Exim 4.68) (envelope-from ) id 1Jyj7s-0007Px-3o; Wed, 21 May 2008 08:52:45 +0100 Message-ID: <4833D4C7.8040809@doc.ic.ac.uk> Date: Wed, 21 May 2008 08:52:39 +0100 From: Martin Berger User-Agent: Thunderbird 1.5.0.9 (X11/20070212) MIME-Version: 1.0 To: David Teller Cc: caml-list Subject: Re: [Caml-list] Re: Where's my non-classical shared memory concurrency technology? References: <4831686F.8010903@doc.ic.ac.uk> <200805192247.09949.jon@ffconsultancy.com> <1211318852.6465.26.camel@Blefuscu> In-Reply-To: <1211318852.6465.26.camel@Blefuscu> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-DCS-Interface-Port: 465 X-DCS-Auth-User: martinb (person) X-Miltered: at concorde with ID 4833D4CA.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; iirc:01 igarashi:01 restrictive:01 idioms:01 typable:01 logics:01 logics:01 wrote:01 typing:01 typing:01 caml-list:01 bugs:03 programming:03 programming:03 concurrency:04 David Teller wrote: > IIRC, there are already type systems which may prevent deadlocks in > pi-calculus. This is true but (1) these typing systems are quite complicated and it will take heroic educational efforts to push such new typing systems into programming mainstream; (2) these typing systems (or at least most of them, the Kobayashi/Igarashi scheme is extremely general) are relatively restrictive and many useful concurrent programming idioms turn out to be not typable. Regarding (1), I think using such typing systems for concurrency is completely unavoidable for a variety of reasons, and they will be adopted in the medium term (in about 10 years), but they are not ready for the mainstream yet. As to (2), extending the typing systems is an active research area, and these problems will be solved eventually. Moreover, recent success in extending Hoare Logics to concurrency mean that we don't have to rely on typing systems alone, instead with can take typing systems of medium complexity to prevent the great majority of concurrency bugs and have logics for rare hard cases. (Well, that's the hope anyway!) Martin