Cyclone

Yesterday I went to a talk at Harvard, titled "Implementation and Evaluation of a Safe Runtime in Cyclone", by Matthew Fluet.

In this talk we outline the implementation of a simple Scheme interpreter and a copying garbage collector that manages the memory allocated by the interpreter. The entire system including the garbage collector is implemented in Cyclone, a safe dialect of C, which supports safe and explicit memory management...

Greg Morrisett, one of the designers of Cyclone, was also present and answered some of the more advanced questions about Cyclone itself.

Cyclone is a "safe" version of C, and it uses static analysis to catch memory leaks. The talk focused on how to write a garbage collector such that the implementation would be accepted by Cyclone's (strict) memory leak detection requirements. First I'll explain how memory leak detection is done in Cyclone, and then I'll explain why it's not trivial to implement a garbage collector using the scheme.

Cyclone's memory leak detection is based on regions. There are several different types of region, but the relevant kind for this talk was the "dynamic" kind. The main characteristics of dynamic regions are that you can allocate new objects into them incrementally, but they have to be freed all at once in one big batch. Perfect for a stop-and-copy garbage collector.

Cyclone restricts the operations you can perform on regions so it can guarantee that you don't leak regions, and that you don't dereference data within a region after it has been freed. This static analysis is based on the idea of capabilities (unforgeable, uncopyable unique handles). Briefly, all the data in a Cyclone program is statically tagged with the region it belongs to (the tag is part of the type, so "an integer in region 1" is different than "an integer in region 2"). You can't actually *use* the data in a region unless you present the requisite capability to the compiler (each region has its own capability). This is done syntactically, kind of like this:

present (region_capability) {
    ... data in the region can be accessed here ...
}
... but not here...

Note that I used my own syntax here. The actual syntax used by Cyclone seems less intuitive to me.

The Cyclone compiler makes it impossible to leak regions by making it illegal to let a capability go out of scope. It also prevents you from referencing previously-freed memory by revoking the capability for the region as soon as you free it. It's actually a pretty simple and straightforward scheme, so if it seems confusing it's probably because I've explained it poorly.

The garbage collector that Matthew Fluet implemented uses a simple stop-and-copy scheme. In other words it takes an old heap, traces through it to find memory still in use, copies that the memory to the new heap, and leaves a "forwarding pointer" in the old heap so that the garbage collector can handle cycles correctly.

It's the forwarding pointers that make things difficult. Because all datatypes have an embedded region name which specifies what region they belong to, it makes it difficult to come up with a type name for the forwarding pointers. Matthew had a very amusing slide that illustrated this. You end up with a type like this:

A pointer to a block in the region after this one, which has a pointer to a block in the region after the one after this one, which has a pointer to a block in the region after the one after the one after this one, which has a pointer to a block in the region after the one after the one after the one after this one, which has ...

To get around this, they introduced a new primitive into the Cyclone runtime, which lets you express this kind of recursion. There was some explanation about how they "used an existential to prime the pump", and some other feature which made some of the verbosity in the type signature become implicit... but I didn't really follow that part.

However what I did glean from the discussion was that Cyclone's straightforward memory leak detection algorithm doesn't lead to a small, well-defined interface. Case in point: in order to implement a garbage collector they had to extend the runtime. It was a small function (only 5 lines of code) but nevertheless it was not possible at the user level. In effect, they had to introduce a new proof rule into the type system. That's disturbing to me -- it means the type system is incomplete. And these are smart people, so if it wasn't complete to start with, that probably means it'll never be complete.

What's even more disturbing is that at the end of the talk, Norman Ramsey asked how they would implement a generational garbage collector. And the answer was, "We haven't figured out how to do that yet... it may require dependent types." Eeek! Suddenly I realized at a deep level that advanced type systems are equivalent to mathematical proofs, and that if you start trying to prove too much about such an unpredictable beast as a program, it will resist you with a vengence.

Just imagine trying to explain to a systems programmer that the reason they can't implement a "simple" generational GC scheme is because that would require that the type checker be extended to support dependent types. They'll look at you like you have three heads, and then they'll toss you and your silly little language into /dev/null.

Posted on February 19, 2004 06:42 PM
More languages articles

Comments

Suddenly I realized at a deep level that advanced type systems are equivalent to mathematical proofs...

This is a deep observation: it's the Curry-Howard isomorphism, which shows the relationship between types and programs on the one hand and logical propositions and their proofs on the other.

Just imagine trying to explain to a systems programmer that the reason they can't implement a "simple" generational GC scheme is because that would require that the type checker be extended to support dependent types.

That's a little unfair: just because something requires dependent types doesn't mean it's infeasible. There are a number of restricted forms of dependent types that are still decidable, e.g., Dependent ML. On the other end of the spectrum there are languages such as Cayenne that abandon the requirement of decidability in the type checker and allow full dependent types. And then there's things like Haskell's type classes, which allow you to simulate some aspects of dependent types.

However, I don't disagree with you: statically predicting the behavior of a program is just plain hard. (Rice's theorem is one such slap in the face.) Striking a balance between a type system generous enough to allow most "good" programs and powerful enough to disallow most "bad" programs seems to be really, really difficult.

...if you start trying to prove too much about such an unpredictable beast as a program it will resist you with a vengeance.

Well said!

Posted by: Dave Herman at February 19, 2004 10:23 PM

Thanks for the summary Kim. As Dave notes in his comment, the Curry-Howard isomorphism shows a relationship between programs/type systems and logical propositions/proofs. The upshot of that isomorphism is that Godel's incompleteness theorem applies to type systems. Godel's theorem says that a proof system cannot be both complete and correct. Because of the isomorphism we then know that a programming language's type system cannot be both complete and correct. That is, every type system will either prevent you from doing some of the things you ought to be able to do; or it will allow you to do things you shouldn't.

Mostly, designers of statically type-checked languages aim for the first approach, guaranteeing that all programs that pass the type checker are typesafe. This can usually be done in such a way that users don't feel too enslaved. Despite good efforts, however, many languages (and probably even more compilers) have type checkers that give their seal of approval to unsafe code. I know, for example, that it is possible to do type-unsafe things in Java in limited cirucmstances involving subtypes and arrays. This is by design of the Java Virtual Machine. But while these kinds of holes sound dangerous, they are mostly of theoretical significance since the circumstances where they arise are, well, super mega weird.

As for you last paragraph, "Just imagine trying to explain to a systems programmer...", this is why weak type systems are useful and popular. Cyclone sounds like it's trying to add a strong type system feature (safe memory allocation) into a weak type system (C), and there's bound to be some impedance mismatch there.

By the way, I learned of your blog from John Sequeira, who I met at a going-away party for Gregor. I recently started my first software engineering job out of college and am enjoying your writing.

Posted by: Shimon Rura at February 20, 2004 10:40 AM

These Women's Classsic Tall 5815 Boots in pink flower print can either be worn at their normal height if you want Ugg boots, but in order for you to create a more casual look to what you are wearing they can be pushed down Women's UGG Classic Tall 5815 Boots in Baked Clay

Posted by: ugg boots on sale at October 27, 2009 02:37 PM

Eliminating the need for the extra trouble to wear ugg boots uk
ugg boots saleuggs, in the extreme sports, look for happiness in life, with UGG Classic boots and nike sb showed off your tall body, do not worry about being laughed at, dancing new style ugg australia and nike sb dunk . The flavor of life that is colorful, there are Christian Louboutincheap nike dunksUGG cardy boots、and nike sb for sale also used fear to creep away money from your pocket Mody ? Love beauty, you might even love UGG Classic tall bootsUGG Nightfall bootsUGG Classic short bootsnew nike sb。There are an infinite high power drivers of popular front ugg boots saleugg saleuggsnike dunkdiscount ugg bootsnike dunk sb, our website also have UGG Nightfall bootsbutton ugg bootsbailey button uggugg button bootsbailey button bootsnike dunk midnike dunk highChristian Louboutin Boots, pick your favorite, do not hesitate!

Posted by: ugg boots sale at November 12, 2009 04:02 AM

People all over the world know the abercrombie and fitch,but not everyone really knows how fashion the abercrombie is,hollister is the Legend maker. Everybody wears the hollister clothing would be the abercrombie mensand the abercrombie womens, if you want know you can search the Ruehl No.925 or abercrombie outlet in the www.google.com .

Posted by: anf at November 13, 2009 12:37 AM

Uggs on sale now.UGG Classic Cardy Boot makes me different form the other

girls. The UGG Bailey Button Boot is a good choice for female.

Posted by: ugg classic cardy boots at November 16, 2009 11:40 PM

Louis Vuitton , commonly referred to as LV Comes First In 2009 World's Top Ten Brands and Mother Shopping With LV Bag!, or sometimes shortened to Journey On LV has become one of the most Sofia Coppola Design Louis Vuitton Bags Agendas luxurybrands Louis Vuitton Flagship Store Opened In California.

Posted by: 1 at November 17, 2009 01:21 AM

UGG Bailey Button bootsis a new style in 2009.The classic cardy uggs boots is another hot boots that worth of buying.And the classic tall ugg boots will make your winter amusing.And now uggs on sale,if you are looking for such a boot,the ugg boots is good choice this year.

Posted by: UGG Bailey Button Boots at November 17, 2009 02:08 AM

I love Women's UGG Classic Cardy Boot 5819 very much. And the new style UGG Mayfaire Boots is aslo a good choice this year.

Posted by: UGG Bailey Button Fancy Boots at November 17, 2009 03:10 AM

I like this post, thank you. and i Just got my ugg boots! They are absolutely beautiful, and the quality is just amazing. No wearing them in, no blisters just absolutely snug strait out of the box. Lol. Uggs boots on sale! So pretty! I will pair them with my new jeans.

Posted by: uggs at November 17, 2009 08:03 PM

lxjuan08ed hardyis a famous ed hardy store which sell directly ed hardy clothing, shoes, boots, swim suit and other cheap ed hardy.

Browse through our catalogue of hundreds of ed hardy clothing,Ed hardy Shirt,Ed hardy ... Buy Ed Hardy today for a gift, for a friend, or for yourself.

Posted by: ed hardy at November 18, 2009 03:58 AM

99.html">ugg mayfaire boots

, nice out fit.good

Posted by: 4t35 at November 19, 2009 08:02 PM

We are the best online sales for the china wholesale . Here you can have a large of choices of kinds Ugg Boots,Converse Shoes,Timberland Boots,puma shoes,Nike Shox Shoes ,Nike Dunk SB Shoes,Nike Air Max,Links Of London,Tiffany Jewelry,Dior Handbags?,jimmy choo handbags ,Cartier Watches, 8GB Mp4 Players,Bluetooth Car DVDs. All our cheap online cheap goods are high quality and original packages, and best service. We offer our customers the best service, 7 days arrive at your door.Enjoy your easy and happy shopping with us.

Posted by: cheap goods sale. at November 19, 2009 10:01 PM

Do you like sports? If you like it,the NIke Air Max TN and Nike Air Max 360 is a good choice for you.And now the there is a good news,CheapNike Air Max running Shoes is waiting for you.I think The New Nike Air MAX 2009 Running Shoes makes you great comfortable.

Posted by: Nike Air Max shoes at November 20, 2009 03:28 AM

xiaorong Auction house Antiquorum auctioned off a very rare vintage chronograph Patek Philippe that
replica watches
replica watches
replica Jaeger LeCoultre watches


replica watches
replica watches
replica A.Lange&Sohne watches

replica watches
replica watches
replica Breitling watches

Posted by: replica Piaget watches at November 21, 2009 05:49 AM

Your article is write very well, I like it very much ~
ghd Hair Straightener
ghd Hair Straighteners
ghd straighteners
GHD
hair straighteners
bose in ear headphones
bose on ear headphones
bose headphones
nike sb dunks
nike dunks
I wish you have a wonderful day!Thank you.

Posted by: ghd straighteners at November 22, 2009 08:51 PM

Timeberland boots on sale now! Do you want moreTimeberland boots information?Just move your mouse and press it to our Timberland shoes online store.

Posted by: Timberland uk at November 22, 2009 11:16 PM

Laptop Battery Laptop Battery Laptop Batteries
Laptop Batteries discount laptop battery
discount laptop battery
notebook battery notebook battery
computer battery computer battery
replacement laptop battery replacement laptop battery
notebook batteries notebook batteries

Posted by: Laptop Battery at November 23, 2009 09:59 PM

The street wear for the street smart speaks a lot about the fashion Christian Louboutin concepts of ed hardy men Line. The suave cuts and colors in the ed hardy t shirts Hoodies has become a popular flair among those who choose to mellow on their daily garb. The sneakers and ed hardy clothes are complemented by the ed hardy sale with its intricate vintage prints. The young professionals who choose not be held captives of edhardy
and casual look of collars and slacks opt for ed hardy t shirt , shirts and hoodies for that relaxed and casual feel. ed hardy outlet is the normal look preferred by the hippies, artists and yuppies alike.


Posted by: ed hardy at November 25, 2009 03:45 AM

Ugg Classic Cardy

Boots

Ugg Classic Tall

Boots

Ugg Classic Short

Boots

Posted by: topuggshoes at November 26, 2009 02:56 AM

chaoying nfl jerseys
Giants Jerseys
Patriots Jerseys

Posted by: jerseysleague at November 29, 2009 04:20 AM

Paul Smith has been collaborating with a few different organizations recently and his latest venture sees him teaming up with Japanese bicycle saddle, Paul Smith bag, on a limited edition leather saddle. The release features Smith’s signature stripes where only 20 will be available at Paul Smith Clothing store in Japan and 8 at the Floral Street store in London. Get on it quick

Posted by: fdasf at November 29, 2009 11:16 AM

Just wanted to say great job with the blog, today is my first visit here and I’ve enjoyed reading your posts so far
ugg bailey button
Wow, my ugg classic mini will not be coming off now! I’ve had them on for 12hrs strait and I do not want to take them off. Thanks for everything, well worth the wait.

Posted by: ugg bailey button boots at November 30, 2009 05:57 AM

Spring is near,every girl wants to be the bride in the special season.They are eager to put on beautiful Wedding Dresses or the Bridal gowns.During the day the Wedding gowns is the good choose,and the night,if you want radiant,you need the Evening gowns.
About the bridesmaid,they have to wear Bridesmaid Dresses in order to avoid grab limelight with the bride.And the Flower Girl has the Flower Girl Dresses,too.In the wedding,the Cocktail Dresses and the Evening Dresses is necessary,too!And remember,the Wedding Dress of the Bridal Dress must be the most glaring!

Posted by: weddingdressclub at December 1, 2009 12:26 AM

Gucci is famous as top quality, Louis Vuitton Tivoli PM luxurious, modern, and sexy luxury goods. Louis Vuitton Replica Tivoli PM It is a symbol of status and wealth. From time to time, Gucci belt is favored by most of people very much.As we know, Gucci belts stand for fashion trend,
Louis Vuitton Tivoli PM Replica popular elements, culture, conciseness gucci and noble. As a gentle and fashion business man or woman, Gucci belt is your best choice. Gucci commercial belts adopt real leathers, and the leathers have high hardness, toughness and scratch resistant. Belt buckles adopt high quality CTB alloy, the golden and silver color of them will never be faded. You like casual clothes and belts, because casual living Speedy 25 lifestyles focus on the simple pleasures of life. We believe that you will not hesitate to choose Gucci belt. Gucci casual belts own fashion and lovely style, bright color. The material of belt is high quality real leather or durable PU leather. Therefore, if you own this kind of Gucci casual belt, you will become a popular star.

Posted by: fanqin at December 1, 2009 01:01 AM
Post a comment









Remember info?




Prove you're human. Type "human":