From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p19L1CHd010572 for ; Wed, 9 Feb 2011 22:01:12 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: An4BAPCOUk3RVdivkGdsb2JhbACXCYY0AYgRCBYBAQEJCQwHEQQgoWaKDIIXhGcviFkBAQMFhVcEgWKKDog1Og X-IronPort-AV: E=Sophos;i="4.60,447,1291590000"; d="scan'208";a="91002537" Received: from mail-qy0-f175.google.com ([209.85.216.175]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 09 Feb 2011 22:01:06 +0100 Received: by qyk8 with SMTP id 8so1627540qyk.6 for ; Wed, 09 Feb 2011 13:01:05 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc:content-type; bh=b7uZZdF/u3TFFAfjxpPyfJOe2Hoqjg00Et6EwCKRp1s=; b=xWSzD717KFXsCs7bGEzeOxajruA0Q7GlEfoN+xwQ6GqJA5nCzR7UahwZjrUbtpxjgR noQ6o8EFuuNbi//qa/W9BshUajwSCiYzczVdzvrmerksa1in4PWHX7MmIZIVuH3STo8w epk5klSm8MalXmqR44tlXUfhvuqkxi8EZycCw= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=j6QjXoGIdNAIw/DvZ95RtJHGA6B2dak1rfNtmPiCHdf6q2mVZoyshSvIB55iKQBTfm CNsAsnAsGvrpVxyDp2U6ZE7NGg1IkWH6eoyD2vSaLdjdYx8ogW8Ov3kkUErBIOdMUriv RKTadYOsuQS5udeZuAM4n1V5WR+ZgvwNDCoAU= Received: by 10.229.249.203 with SMTP id ml11mr5162874qcb.199.1297285264764; Wed, 09 Feb 2011 13:01:04 -0800 (PST) MIME-Version: 1.0 Received: by 10.229.101.199 with HTTP; Wed, 9 Feb 2011 13:00:44 -0800 (PST) In-Reply-To: <06339C3C-7F90-47F9-895D-3E2CA49A4C5F@cap-lore.com> References: <50AF76A1-30E0-4735-AFB2-88BB603899CE@ezabel.com> <06339C3C-7F90-47F9-895D-3E2CA49A4C5F@cap-lore.com> From: Gabriel Scherer Date: Wed, 9 Feb 2011 22:00:44 +0100 Message-ID: To: Norman Hardy Cc: orbitz@ezabel.com, caml-list@inria.fr Content-Type: multipart/alternative; boundary=0016e64caa7e60eea1049bdfc39e Subject: Re: [Caml-list] Scoped Bound Resource Management just for C++? --0016e64caa7e60eea1049bdfc39e Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: quoted-printable For an example of a language with linear types for resource management, as mentioned by Andreas Rossberg, see ATS : http://www.ats-lang.org/ Of particular interest to the present discussion are the following pages: - Stack allocation : http://www.ats-lang.org/TUTORIAL/contents/stack-allocation.html memory and closures are allocated on the stack, with the type system guaranteeing that such values cannot be referenced after the current function exit - Cairo basics : http://www.ats-lang.org/DOCUMENTATION/ATSCAIRO/HTML/c28.html a small tutorial for programming with the Cairo library; linear types are used to track the cairo resources, which internally -- on the C side -- use reference counting - "Implementing Reliable Linux Device Drivers in ATS" : http://www.ats-lang.org/PAPER/LDD-plpv07.pdf On Wed, Feb 9, 2011 at 9:47 PM, Norman Hardy wrote: > > On 2011 Feb 8, at 15:57 , orbitz@ezabel.com wrote: > > > One of the benefits, in my opinion, of C++ is SBRM. You can reason abo= ut > the lifetime of an object and have an give yourself guarantees about its > clean up. The method of initialization and clean up are also consistent = for > every object in the language. > > > > My questions are: > > 1) Do other people in the FP world consider this to be a good strategy? > > 2) Can this be done in a sane way in a GCd language? > > 3) What are the alternatives in a language like Ocaml? > > Keykos was a platform intended for program agents from diverse and even > hostile interests. > http://cap-lore.com/CapTheory/KK/ > It had an adversarial space allocation technology. > http://cap-lore.com/CapTheory/KK/Space.html > It was an operating system with a space allocation facility that was both > safer and less safe than GC. > It was safer in that it was feasible to write applications therein safe > from space exhaustion. > It was less safe in that programming errors might delete space too soon. > It did not suffer, however, from =91memory safety=92 errors when =91stale > pointers=92 were used. > The behavior of stale pointers was determined and =91threw exceptions=92 = by > default. > Lurking forgotten references that were indeed destined not to be used were > not a problem as in GC. > > Releasing storage was explicit and indeed an extra additional application > burden. > It was also possible for the agent paying for the storage to reclaim the > storage despite access by others. > > The allocation mechanisms were responsible for space on timescales from > milliseconds to years. > > Many complex agreements on data access between parties, positive and > negative, were possible in Keykos, and enforced by mutually trusted softw= are > agents therein. > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa-roc.inria.fr/wws/info/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > > --0016e64caa7e60eea1049bdfc39e Content-Type: text/html; charset=windows-1252 Content-Transfer-Encoding: quoted-printable For an example of a language with linear types for resource management, as = mentioned by Andreas Rossberg, see ATS : http://www.ats-lang.org/

Of particular interest to the presen= t discussion are the following pages:
- Stack allocation : http://www.ats-lang.org/TUTORIAL/contents/stack-alloc= ation.html
=A0 memory and closures are allocated on the stack, with = the type system guaranteeing that such values cannot be referenced after th= e current function exit
- Cairo basics : http://www.ats-lang.org/DOCUMENTATION/ATSCAIRO/HTML/c28.html=
=A0 a small tutorial for programming with the Cairo library; linear= types are used to track the cairo resources, which internally -- on the C = side -- use reference counting
- "Implementing Reliable Linux Device Drivers in ATS" : http://www.ats-lang.org/P= APER/LDD-plpv07.pdf

On Wed, Feb 9, 20= 11 at 9:47 PM, Norman Hardy <norm@cap-lore.com> wrote:

On 2011 Feb 8, at 15:57 , orbitz@ezabe= l.com wrote:

> One of the benefits, in my opinion, of C++ is SBRM. =A0You can reason = about the lifetime of an object and have an give yourself guarantees about = its clean up. =A0The method of initialization and clean up are also consist= ent for every object in the language.
>
> My questions are:
> 1) Do other people in the FP world consider this to be a good strategy= ?
> 2) Can this be done in a sane way in a GCd language?
> 3) What are the alternatives in a language like Ocaml?

Keykos was a platform intended for program agents from diverse and ev= en hostile interests.
http://cap-= lore.com/CapTheory/KK/
It had an adversarial space allocation technology.
h= ttp://cap-lore.com/CapTheory/KK/Space.html
It was an operating system with a space allocation facility that was both s= afer and less safe than GC.
It was safer in that it was feasible to write applications therein safe fro= m space exhaustion.
It was less safe in that programming errors might delete space too soon.
It did not suffer, however, from =91memory safety=92 errors when =91stale p= ointers=92 were used.
The behavior of stale pointers was determined and =91threw exceptions=92 by= default.
Lurking forgotten references that were indeed destined not to be used were = not a problem as in GC.

Releasing storage was explicit and indeed an extra additional application b= urden.
It was also possible for the agent paying for the storage to reclaim the st= orage despite access by others.

The allocation mechanisms were responsible for space on timescales from mil= liseconds to years.

Many complex agreements on data access between parties, positive and negati= ve, were possible in Keykos, and enforced by mutually trusted software agen= ts therein.

--
Caml-list mailing list. =A0Subscription management and archives:
https://sympa-roc.inria.fr/wws/info/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs


--0016e64caa7e60eea1049bdfc39e--