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=AWL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 5E8D5BBC4 for ; Tue, 20 May 2008 23:32:35 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ApoEAKjgMkjAXQIm/2dsb2JhbACvbQ X-IronPort-AV: E=Sophos;i="4.27,517,1204498800"; d="scan'208";a="26427551" Received: from discorde.inria.fr ([192.93.2.38]) by mail4-smtp-sop.national.inria.fr with ESMTP; 20 May 2008 23:32:04 +0200 Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id m4KLVaaV031807 for ; Tue, 20 May 2008 23:32:02 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AnYBAE/eMkjCpx6vlWdsb2JhbACSMQEBAQEJBQYanH8 X-IronPort-AV: E=Sophos;i="4.27,517,1204498800"; d="scan'208";a="12834917" Received: from smtpka.univ-orleans.fr (HELO ka.univ-orleans.fr) ([194.167.30.175]) by mail3-smtp-sop.national.inria.fr with ESMTP; 20 May 2008 23:25:26 +0200 Received: from smtps.univ-orleans.fr (localhost [127.0.0.1]) by ka.univ-orleans.fr (Postfix) with ESMTP id 52C8812AD4A; Tue, 20 May 2008 23:25:25 +0200 (CEST) Received: from [192.168.0.12] (ras75-4-82-235-58-110.fbx.proxad.net [82.235.58.110]) by smtps.univ-orleans.fr (Postfix) with ESMTP id 7AC2C36E5B; Tue, 20 May 2008 23:25:29 +0200 (CEST) Subject: Re: [Caml-list] Re: Where's my non-classical shared memory concurrency technology? From: David Teller To: Berke Durak Cc: Jon Harrop , caml-list In-Reply-To: References: <4831686F.8010903@doc.ic.ac.uk> <200805192247.09949.jon@ffconsultancy.com> Content-Type: text/plain Date: Tue, 20 May 2008 23:27:32 +0200 Message-Id: <1211318852.6465.26.camel@Blefuscu> Mime-Version: 1.0 X-Mailer: Evolution 2.12.1 Content-Transfer-Encoding: 7bit X-Miltered: at discorde with ID 48334338.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; univ-orleans:01 iirc:01 ocaml's:01 cheers:01 0200,:01 berke:01 durak:01 mutable:01 parallelism:01 non-trivial:01 univ-orleans:01 lifo:01 liquidations:98 threads:01 wrote:01 IIRC, there are already type systems which may prevent deadlocks in pi-calculus. And since pi-calculus is essentially the base for CML/OCaml's Event/lwt (I'm not 100% sure for lwt), my guess is that it shouldn't be too hard to get them to work for purely functional threaded code. The missing step would be to detect whether code is purely functional, which is a rather easy task (if tedious). The alternative to that missing step would be to detect whether impurities are localized to each thread -- something which I believe would also be quite feasible, provided you limit side-effects to the use of a well-defined, thread-local, API. Cheers, David On Tue, 2008-05-20 at 00:24 +0200, Berke Durak wrote: > Given that shared, mutable global state accessed with multiple threads > is a recipe for bugs that no amount of data hiding can solve (because > -locking-sections-don't-compose-), > did anyone invent and implement a usable type or other system for > making concurrency > and parallelism safe? > > If the answer is STM, please show me some non-trivial application that > uses it, preferably > in an impure language. -- David Teller Security of Distributed Systems http://www.univ-orleans.fr/lifo/Members/David.Teller Angry researcher: French Universities need reforms, but the LRU act brings liquidations.