Showing content from http://www.cs.washington.edu/homes/djg/slides/grossman_cyclone_jpl_05.ppt below:
ÐÏࡱá>þÿ Þ5þÿÿÿÜÝÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿèÎé(à8Ø òú/È 0ÒÕ0·DTimes New Roman©Ñ´ÕÕì 0´ÕWo 0·DArialNew Roman©Ñ´ÕÕì 0´ÕWo 0" ·DCourier Newman©Ñ´ÕÕì 0´ÕWo 010·DWingdingswman©Ñ´ÕÕì 0´ÕWo 0¤ `ÿÿÿÿ¥ .© @£nÿý?" dd@ÿÿïÿÿÿÿÿÿ @@`` ðüð@~6/ /7ZM)@280c //2 0/,+*)($3')&% :4"$3#!.2- ð0A¿ÀÅAÿpñÿ3ÌfÌfÿÿÿfÿ@ñ÷ð8óóÐÑððnÊ;ÇÊ;úgþý4XdXdì 0¨Õÿÿÿ¦ÿÿÿpûppû@<ý4!d!d® 0dÙªÑ<ý4dddd® 0dÙªÑ<ý4BdBd® 0dÙªÑÿ N0º___PPT10 ÀÀº___PPT9ð®è¯¬`ÿÿÿÿÿÿ¯¬Xÿÿ?ÙdÚ-º11 January 2005 º*Dan Grossman: CycloneOÙ Ú=ðßzó¨4Cyclone: A Memory-Safe C-Level Programming Language ¡"53 Ìfþ¨¬Dan Grossman University of Washington Joint work with: Trevor Jim AT&T Research Greg Morrisett Harvard University Michael Hicks University of Maryland¡:'(&Ìfþó¨A safe C-level language¨ Cyclone is a programming language and compiler aimed at safe systems programming C is not memory safe: void f(int* p, int i, int v) { p[i] = v; } Address p+i might hold important data or code Memory safety is crucial for reasoning about programs ¡S9h:ÿ3þÿ3þ þþþþ $ 6óà "Caller s problem?ª¨Ã void g(void**, void*); int y = 0; int *z = &y; g(&z,0xBAD); *z = 123; Might be safe, but not if g does *x=y Type of g enough for code generation Type of g not enough for safety checking¡$N v þþ þ!%ª> s& óë'¨Safe low-level systems¨8For a safety guarantee today, use YFHLL Your Favorite High Level Language YFHLL provides safety in part via: hidden data fields and run-time checks automatic memory management Data representation and resource management are essential aspects of low-level systems There are strong reasons for C-like languages¡(##D$Y.(ÌfþÌfþÌfþÌfþÌfþ#ÿ3þ! ÿ3þ0 ÿ3þ-óì(¨Some insufficient approaches ®Compile C with extra information type fields, size fields, live-pointer table, & treats C as a higher-level language Use static analysis very difficult less modular Ban unsafe features there are many you need them¡!U!T óǨCyclone in brief *A safe, convenient, and modern language at the C level of abstraction Safe: memory safety, abstract types, no core dumps C-level: user-controlled data representation and resource management, easy interoperability, manifest cost Convenient: may need more type annotations, but work hard to avoid it Modern: add features to capture common idioms New code for legacy or inherently low-level systems ¡ôGZZ6ZZFÿþÿþ. e ; '6óȨThe plan from here êExperience with Cyclone Benchmarks, ports, systems, compiler, & All on Earth so far Jð Not-NULL pointers Type-variable examples generics region-based memory management Brief view of everything else Related work Really just a taste of Cyclone¡ÂZ>Z)Z(Z-Z"Z< (-"óɨStatus ® Cyclone really exists (except memory-safe threads) >150K lines of Cyclone code, including the compiler gcc back-end (Linux, Cygwin, OSX, Mindstorm, & ) User s manual, mailing lists, & Still a research vehicle ¡À4¢34 0 ª ?óʨ Evaluation¨æ Is Cyclone like C? port code, measure source differences interface with C code (extend systems) What is the performance cost? port code, measure slowdown Is Cyclone good for low-level systems? write systems, ensure scalability ¡Ê" N" '" "N '"óË ¨Code differences¨Porting not automatic, but quite similar Many changes identify arrays and lengths Some changes incidental (absent prototypes, new keywords)¡óÌ ¨Run-time performance¨ÐRHLinux 7.1 (2.4.9), 1.0GHz PIII, 512MRAM, gcc2.96 -O3, glibc 2.2.4 Comparable to other safe languages to start C level provides important optimization opportunities Understanding the applications could help¡LED,6*óͨLarger program: the compiler¨Ö Scalable compiler + libraries (80K lines) build in < 30secs Generic libraries (e.g., lists, hashtables) clients have no syntactic/performance cost Static safety helps exploit the C-level I use &x more than in C ¡¼ 4,,( 3 ,+ ( óÎ ¨Other projects¨oOpen Kernel Environment [Bos/Samwel, OPENARCH 02] MediaNet [Hicks et al, OPENARCH 03]: RBClick [Patel/Lepreau, OPENARCH 03] STP [Patel et al., SOSP 03] FPGA synthesis [Teifel/Manohar, ISACS 04] Maryland undergrad O/S course (geekOS) [2004] Windows device driver (6K lines) Only 100 lines left in C But unrecoverable failures & other kernel corruptions remain ¡PWPP ' !Wªt =,óÒ¨The plan from here ,Experience with Cyclone Not-NULL pointers Type-variable examples generics region-based memory management Brief view of everything else Related work ¡zA(-(-óÓ¨Not-null pointersª óÔ¨Example ÌFILE* fopen(const char@, const char@); int fgetc(FILE@); int fclose(FILE@); void g() { FILE* f = fopen( foo , r ); while(fgetc(f) != EOF) {& } fclose(f); } Gives warning and inserts one null-check Encourages a hoisted check¡Ü¢ZEZþ þ þþ þBDªP zóÕ¨A classic moral¨LFILE* fopen(const char@, const char@); int fgetc(FILE@); int fclose(FILE@); ¡Mþ þ þ ª,1 óÖ!¨Key Design Principles in Action¨SUse types to express invariants Preconditions for arguments Properties of values in memory Use flow analysis where helpful Lets users control explicit checks Soundness + aliasing limits usefulness Users control data representation Pointers are addresses unless user allows otherwise Often can interoperate with C more safely just via types¡° Z;Z ZJZ"Z4Z9Z ; #'"49óò. (It s always aliasing¨¿But can avoid checks when compiler knows all aliases. Can know by: Types: precondition checked at call site Flow: new objects start unaliased Else user should use a temporary (the safe thing)¡ C}Àª 3óó/ (It s always aliasing¨¿But can avoid checks when compiler knows all aliases. Can know by: Types: precondition checked at call site Flow: new objects start unaliased Else user should use a temporary (the safe thing)¡ C}Àª 3óñ-¨The plan from here ,Experience with Cyclone Not-NULL pointers Type-variable examples generics region-based memory management Brief view of everything else Related work ¡pA(-*(-óØ ( Change void* to `a ¡:¨struct Lst { void* hd; struct Lst* tl; }; struct Lst* map( void* f(void*), struct Lst*); struct Lst* append( struct Lst*, struct Lst*);¡\ ;þ1þ!óÙ¨Not much new here¨Closer to C than C++, Java generics, ML, etc. Unlike functional languages, data representation may restrict `a to pointers, int why not structs? why not float? why int? Unlike templates, no code duplication or leaking implementations Unlike objects, no need to tag data¡Ú/S)f/"N"c""c"c" " f"ª¦ióÚ¨Existential types Programs need a way for call-back types: struct T { void (*f)(void*, int); void* env; }; We use an existential type (simplified): struct T { <`a> void (@f)(`a, int); `a env; }; more C-level than baked-in closures/objects ¡+ZA0ZZ*ZA0Z,8ZZ+>" ÿþgÿþGÿþgÿ3þ gÿ3þ, "óÛ¨Regions a.k.a. zones, arenas, & Every object is in exactly one region Allocation via a region handle Deallocate an entire region simultaneously (cannot free an object) Old idea with recent support in languages (e.g., RC, RTSJ) and implementations (e.g., ML Kit)¡²|Z*ZZ_Z&7 _ª>`F. %óܨCyclone regions [PLDI 02]¡ heap region: one, lives forever, conservatively GC d stack regions: correspond to local-declaration blocks: {int x; int y; s} growable regions: scoped lifetime, but growable: {region r; s} allocation routines take a region handle handles are first-class caller decides where, callee decides how much no handles for stack regions¡m4B K (*þþ#þ".ÿ3þªb,1\óÝ (That s the easy part¨cThe implementation is really simple because the type system statically prevents dangling pointers ¡hd ÿþóÞ¨The big restriction ÎAnnotate all pointer types with a region name (a type variable of region kind) int@`r means pointer into the region created by the construct that introduces `r heap introduces `H L:& introduces `L {region r; s} introduces `r r has type region_t<`r> compile-time check: only live regions are accessed by default, function arguments point to live regions ¡PS$B² 35"" GgI"c"bc"c "cgþc "c" " c " c c 3b5bcªP¡''jóߨRegion polymorphism øApply what we did for type variables to region names (only it s more important and could be more onerous) void swap(int @`r1 x, int @`r2 y){ int tmp = *x; *x = *y; *y = tmp; } int@`r sumptr(region_t<`r> r,int x,int y){ return rnew(r) (x+y); }¡BkM EkCGþCgcgþcgcgþ cgþ cCC g ÿþ c g þ c g ÿþ c g þ c g þ c g þ c ª,Óóà¨Type definitions¨Kstruct ILst<`r1,`r2> { int@`r1 hd; struct ILst<`r1,`r2> *`r2 tl; }; ¡ L CgÿþC g ÿþCgÿþCgÿþ C $g$ÿþ(C(,g,ÿþ 0C000óá ¨Region subtyping ÒIf p points to an int in a region with name `r1, is it ever sound to give p type int*`r2? If so, let int*`r1 < int*`r2 Region subtyping is the outlives relationship {region r1; & {region r2; & } & } LIFO makes subtyping common ¡$[M!gÿþ g ÿþ CgÿþoÿþçÿGCgÿþnÿþçÿoÿþçÿ B F B $ C B C ª>ª óâ"¨Regions evaluationª ÆLIFO regions good for some idioms awkward in C Regions generalize stack variables and the heap Defaults and inference make it surprisingly palatable Worst part: defining region-allocated data structures Cyclone actually has much more [ISMM 04] Non-LIFO regions Unique pointers Explicitly reference-counted pointers A unified system , not n sublangages ¡/xf6)p/f6 a ªWóã#¨The plan from here ,Experience with Cyclone Not-NULL pointers Type-variable examples generics region-based memory management Brief view of everything else Related work ¡pA(-A( óä$¨Other safety holes JArrays (what or where is the size) Options: dynamic bound, in a field/variable, compile-time bound, special string support Threads (avoiding races) vaporware type system to enforce lock-based mutual exclusion Casts Allow only up casts and casts to numbers Unions Checked tags or bits-only fields Uninitialized data Flow analysis (safer and easier than default initializers) Varargs (safe via changed calling convention)¡î#X=+!;.#X=+ ! ;.ª> A'óå%¨And modern conveniences æ30 years after C, some things are worth adding& Tagged unions and pattern matching on them Intraprocedural type inference Tuples (like anonymous structs) Exceptions Struct and array initializers Namespaces new for allocation + initialization ¡Z0xÃ0 "ª>{ Hóê&¨Plenty of work remains¨ÓCommon limitations: Aliasing Arithmetic Unportable assumptions (But interoperating with C is much simpler than in a HLL) Big challenge for next generation: guarantees beyond fail-safe (i.e., graceful abort)¡X,:Y^rª( ¢óϨRelated work: making C safer ÊCompile to make dynamic checks possible Safe-C [Austin et al.], RTC [Yong/Horwitz], ... Purify, Stackguard, Electric Fence, & CCured [Necula et al.] performance via whole-program analysis less user burden less memory management, single-threaded Control-C [Adve et al.] weaker guaranty, less burden SFI [Wahbe, Small, ...]: sandboxing via binary rewriting ¡ð(ZmZ`ZpZZ(1` # ª>@aóí*¨Related Work: Checking C code fModel-checking C code (SLAM, BLAST, & ) Leverages scalability of MC Key is automatic building and refining of model They assume (weak) memory safety Lint-like tools (Splint, Metal, PreFIX, & ) Good at reducing false positives Cannot ensure absence of bugs Metal particularly good for user-defined checks Cqual (user-defined qualifiers, lots of inference) Better for unchangeable code or user-defined checks (i.e., they re complementary)¡Â'm+o3S'Q+!H2 Sª,´tóð,¨Related work: higher and lower ¸Adapted/extended ideas: polymorphism [ML, Haskell, & ] regions [Tofte/Talpin, Walker et al., & ] safety via dataflow [Java, & ] existential types [Mitchell/Plotkin, & ] controlling data representation [Ada, Modula-3, & ] Safe lower-level languages [TAL, PCC, & ] engineered for machine-generated code Vault: stronger properties via restricted aliasing ¡Á)'4À)&4óѨSummary òCyclone: a safe language at the C-level of abstraction Synergistic combination of types, flow analysis, and run-time checks A real compiler and prototype applications Properties like not NULL , has longer lifetime , has array length & now in the language and checked Easy interoperability with C allow smooth and incremental move toward memory safety in theory at least¡zg7 E + g Uóî)¨ Availability Like any language, you have to kick the tires : www.research.att.com/projects/cyclone Also see: Jan. 2005 C/C++ User s Journal USENIX 2002 Conversely, I want to know NASA s C-level code needs Maybe ideas from Cyclone will help Maybe not Either way would be fascinating ¡¢1' +5-!1%Ìfþ +ª1Ìóæ¨ r[Presentation ends here some auxiliary slides follow]¡::óç¨Example in Cyclone¨void f(int@{`j} p, tag_t<`i> i, int v ; `i < `j){ p[i] = v; } Note: regions and locks use implicit defaults (live and accessible)¡ÌIEþÿ3þ ÿ3þ ÿ3þFª,"Róô0¨Some other problems \One safety violation typically renders all program properties potentially irrelevant So prohibit: incorrect casts, array-bounds violations, misused unions, uninitialized pointers, dangling pointers, null-pointer dereferences, dangling longjmp, vararg mismatch, not returning pointers, data races, & ¡,dZËZdË/ð¨ó^óÅ%óÐ&óè'óé(óï)PÿÿÿêøÈ ï `ð ÿÿÿÿÿÿÿÿÿÿ`ð ÿÿÿÌ33ÌÌÌÿ²²²`ð ÿÿÿ333ÝÝÝMMMêêê`ð ÿÿÌff3333ÌÿÌf`ð ÿÿÿÿÌfÿÌÌÀÀÀ`ð ÿÿÿÀÀÀfÿÿ`ð ÿÿÿ3ÿÿÌÌ̲²²£>ÿý?" dd@ÿÿïÿÿÿÿÿÿ$£zÿý?" ddØ@ÿÿïÿÿÿÿÿÿ Ô " Ð@ ð`» £nÿý?" dd@ÿÿïÿÿÿÿÿÿ @@``P£V @ ` `£ p£>£>ùP 0 ÞðÖð ðnð( ð ð ðà ð ð6PäÑ¿Àÿ "ñ¿ðÀ°ÐðÃÑ ðT¨ Click to edit Master title style¢!ª !ð$ ð ð0çÑ¿Àÿ "ñ¿ðð°ÐðÃÑ ð¨RClick to edit Master text styles Second level Third level Fourth level Fifth level¢! ª Sðâ ð ð0ÜëÑ¿Àÿ "ñ¿ðÀ°`àðÃÑ ð\ *¡øªðä ð ð0ñÑ¿Àÿ "ñ¿ðÀ @àðÃ Ñ ð^ * ¡úªð`B ð sð*D¿ÀËÔÿ"ñ¿ð0àp0ðä ð ð0$õÑ¿Àÿ "ñ¿ð´ÐàðÃÑ ð^ *¡ØªðH ð ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²² º&dan_design_templateî[ï ùPØ óðë@ððð( ð ððà ð ð6tár¿Àÿ "ñ¿ð °ÐpðÃr ðT¨ Click to edit Master title style¢!ª !ðÝ ð ð0Ýr¿Àÿ "ñ¿ð ` à ðÃr ðW¨#Click to edit Master subtitle style¢$ª $ðÞ ð ð0 s¿Àÿ "ñ¿ð`°`ðÃr ðX *¡øªðà ð ð00%s¿Àÿ "ñ¿ð`°Ððà s ðZ *¡úªðà ð ð0¸(s¿Àÿ "ñ¿ð` ÐðÃs ðZ *¡Øªð`B ð sð*D¿ÀËÔÿ"ñ¿ð0àp0ð`B ð sð*D¿ÀËÔÿ"ñ¿ð@àp@ðH ð ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²ðñ 0 ð`ð0ðð( ð ð0ð ð0 ÓðNxsgk´µgk´µ¿¿Àÿ ðv$ðà s ðn *¡ ùª ¦ñJ%%JJooð ð0 ÓðNü
sgk´µgk´µ¿¿Àÿ ð 8$ðÃs ðp *¡ øª ¦ñJ%%JJooðd ð0 cð$¿ÿ ?ð·æRH ðÃsð4 ð0 ÓðN`sgk´µgk´µ¿¿Àÿ ðÚ Lì!ðÃs ð¨RClick to edit Master text styles Second level Third level Fourth level Fifth level¢! ª Sð ð0 ãðT ¢sgk´µgk´µ¿¿Àÿ ð´vØðà s ðn *¡ úª ¦ñJ%%JJooð ð0 ãðTp¢sgk´µgk´µ¿¿Àÿ ð´Â 8ØðÃs ðp *¡ ت ¦ñJ%%JJooðH ð0 ð0ßjBÁ¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²80º___PPT10ë.ÚñÄPÿc_Ép ðø@ððð( ð ðð ð ÓðN(ggk´µgk´µ¿¿Àÿ ðv$ðà { ðv *¡ ùª¦ñJ%%JJooð ð ÓðNThgk´µgk´µ¿¿Àÿ ð 8$ðÃ{ ðx *¡ øª¦ñJ%%JJooð ð ãðT]gk´µgk´µ¿¿Àÿ ð´vØðà { ðv *¡ úª¦ñJ%%JJooð ð ãðTøEgk´µgk´µ¿¿Àÿ ð´Â 8ØðÃ{ ðx *¡ ت¦ñJ%%JJooðH ð ð0ßjBÁ¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²80º___PPT10ë.ÚñÄܱ`îïùPç ð0ðð0ð( ð ððx ð cð$2s¿ÿðð°ÐÀðÃs ð ðx ð cð$P3s¿ÿðPPÐ ðÃs ð ðH ð ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²îï %ùPÿÿÿ ®ð¦ðTð>ð( ð ðTðx ðT cð$(¿ÿ ðÀ°Ððà ð ð ðT cð$Ô¿ÿ ðð°0ðà ð¦ðH ðT ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²îï ù@ç ððð`ð0ð( ð ð`ðx ð` cð$¿ÿ ðÀ°Ððà ð ðx ð` cð$T¿ÿ ðð°Ððà ð ðH ð` ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²îï )ùPÿÿÿ ðàðð0ð( ð ððx ð cð$ ¿ÿ ðÀ°Ððà ð ðx ð cð$X¿ÿ ðð°Ððà ð ðH ð ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²îï ùPÿÿÿ ðÐðð0ð( ð ððx ð cð$ð¿ÿ ðÀ°Ððà ð ðx ð cð$x¿ÿ ðð°Ððà ð ðH ð ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²îï ù@ÿÿÿ ðÀðlð0ð( ð ðlðx ðl cð$èÜ¿ÿ ðÀ°Ððà ð ðx ðl cð$¤Ý¿ÿ ðð°Ððà ð ðH ðl ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²îï ù@ÿÿÿ ð°ðpð0ð( ð ðpðx ðp cð$ÐÉ¿ÿ ðÀ°Ððà ð ðx ðp cð$Ê¿ÿ ðð°Ððà ð ðH ðp ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²îï ùPÿÿÿ ð ðtð0ð( ð ðtðx ðt cð$¨Á¿ÿ ðÀ°Ððà ð ðx ðt cð$d¿ÿ ð°` ðà ð ðH ðt ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²îï ùPÿÿÿ ¶ð®ðxðFð( ð ðxðx ðx cð$lo¿ÿ ðÀ°Ððà ð ð ðx cð$Dô¿ÿ ðð°Ððà ð"¦ø @08XðH ðx ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²îõï &ùPÿÿÿ ð
ð##|ðð( ð ð|ðx ð| cð$¸=¿ÿ ðÀ°Ððà ð ðx ð| cð$t>¿ÿ ð Ððà ð ðåðv ðp ð|#ð #"ñ" à ààpð@ð¿ ð| £ð<4¿¿Àÿ?ð@ ðK¨0¡ ¦ø @`ðÍ ð| £ð< ¿¿Àÿ?ð` @ ðY¨ 2 (32=5.5%)¡ ¦ø @`ð ð| £ð< ¿¿Àÿ?ð ` ð (+ 34 (5.8%) 29¡2 "¦ø @`ðà ð| £ð<è¿¿Àÿ?ðã ðO¨ 584¡ ¦ø @`ð× ð | £ð<¸¿¿Àÿ?ðp ã ðc¨ccured-olden-mst (1 of 4)¡ ¦ø @`ðÎ ð | £ð<D)¿¿Àÿ?ð@) ðZ¨1 ¡& ÿ3þ¦ø @`ðË ð| £ð<´1¿¿Àÿ?ð` )@ ðW¨ 12 (261=8.7%)¡ ¦ø @`ðü ð | £ð<43¿¿Àÿ?ð)` ð $+ 273 (9.1%) 245¡2 "¦ø @`ð ð | £ð<À5¿¿Àÿ?ðã) ðN¨3005¡ ¦ø @`ðÑ ð| £ð<àJ¿¿Àÿ?ðp)ã ð]¨mini-httpd (1 of 6)¡ ¦ø @`ðî ð| £ð<pT¿¿Àÿ?ð@I ) ðz¨1 (half of examples)¡4 ÿ3þÿ3þ¦ø @`ðË ð| £ð<\¿¿Àÿ?ð` I@) ðW¨ 41 (216=6.6%)¡ ¦ø @`ðü ð| £ð<f¿¿Àÿ?ðI` ) ð $+ 257 (7.9%) 190¡2 "¦ø @`ð ð| £ð<Pn¿¿Àÿ?ðãI) ðN¨3260¡ ¦ø @`ðÏ ð| £ð< v¿¿Àÿ?ðpIã) ð[¨grobner (1 of 4)¡ ¦ø @`ðÈ ð| £ð<x¿¿Àÿ?ð@ I ðT¨ bugs found¡ ¦ø @`ðÈ ð| £ð<Ü¿¿Àÿ?ð` @I ðT¨ incidental¡ ¦ø @`ðÈ ð| £ð< ¿¿Àÿ?ð` I ðT¨ diff total¡ ¦ø @`ðÈ ð| £ð<ø¿¿Àÿ?ðãI ðT¨ Lines of C¡ ¦ø @`ðÅ ð| £ð<x¿¿Àÿ?ðpãI ðQ¨Example¡ ¦ø @`ð`B ð| ð0¿ÀËo×ÿ ?¿ðp ðZB ð| sð*¿ÀË1ÿ ?¿ðpI IðZB ð| sð*¿ÀË1ÿ ?¿ðp) )ðZB ð| sð*¿ÀË1ÿ ?¿ðp ð`B ð| ð0¿ÀËo×ÿ ?¿ðp ð`B ð| ð0¿ÀËo×ÿ ?¿ðppðZB ð| sð*¿ÀË1ÿ ?¿ðããðZB ð | sð*¿ÀË1ÿ ?¿ððZB ð!| sð*¿ÀË1ÿ ?¿ð` ` ðZB ð"| sð*¿ÀË1ÿ ?¿ð@@ð`B ð#| ð0¿ÀËo×ÿ ?¿ð ðH ð| ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²î¬ï ùPç Dð<pð((ðÔð( ð ððx ð cð$¿ÿ ðÀ°Ððà ð ðx ð cð$Ô¿ÿ ðp0ððà ð ððv ð° ð#ð #"ñ" ðáàpðpðü ð £ð<¨ ¿¿Àÿ?ð À ð $+ 35 30 nogc¡2 "¦ø @`ðß ð £ð<¬+¿¿Àÿ?ð *À ðk¨ ¡2 " "¦ø @`ðî ð £ð<h3¿¿Àÿ?ð IÀ* ðz + 336 196¡2 "¦ø @`ðÄ ð £ð<h=¿¿Àÿ?ð ÀI ðP¨faster¡ ¦ø @`ðà ð £ð<¸C¿¿Àÿ?ðÀ ° ðO¨1.39x¡ ¦ø @`ðà ð £ð<ÈF¿¿Àÿ?ðð ðO¨1.93x¡ ¦ø @`ðò ð £ð<`U¿¿Àÿ?ð° ð ð~ + 34 29¡2 "¦ø @`ðà ð £ð<HP¿¿Àÿ?ð ° ðO¨ 584¡ ¦ø @`ð× ð £ð<0e¿¿Àÿ?ð ðc¨ccured-olden-mst (1 of 4)¡ ¦ø @`ðÕ ð £ð<Hón¿¿Àÿ?ðÀ*° ða¨ ¡& " "¦ø @`ðÇ ð £ð< h¿¿Àÿ?ðð * ðS¨1.02x¡ ÿ3þ¦ø @`ðî ð £ð<Ð~¿¿Àÿ?ð°*ð ðz + 273 245¡2 "¦ø @`ð ð £ð<¿¿Àÿ?ð *° ðN¨3005¡ ¦ø @`ðÑ ð £ð<Ø¿¿Àÿ?ð* ð]¨mini-httpd (1 of 6)¡ ¦ø @`ðà ð £ð<¿¿Àÿ?ðÀI°* ðO¨1.51x¡ ¦ø @`ðà ð £ð<X¿¿Àÿ?ðð I * ðO¨1.94x¡ ¦ø @`ðî ð £ð< ¿¿Àÿ?ð°Ið * ðz + 257 190¡2 "¦ø @`ð ð £ð<À¯¿¿Àÿ?ð I°* ðN¨3260¡ ¦ø @`ðÏ ð £ð<ð·¿¿Àÿ?ðI * ð[¨grobner (1 of 4)¡ ¦ø @`ðÌ ð £ð<äÀ¿¿Àÿ?ðÀ°I ðX¨execution time¡ ¦ø @`ðÌ ð £ð<dÉ¿¿Àÿ?ðð I ðX¨execution time¡ ¦ø @`ðÈ ð £ð<äÊ¿¿Àÿ?ð°ð I ðT¨ diff total¡ ¦ø @`ðÈ ð £ð<øÙ¿¿Àÿ?ð °I ðT¨ Lines of C¡ ¦ø @`ðÅ ð £ð<¬á¿¿Àÿ?ð I ðQ¨Example¡ ¦ø @`ð`B ð ð0¿ÀËo×ÿ ?¿ð°ðZB ð sð*¿ÀË1ÿ ?¿ðI°IðZB ð sð*¿ÀË1ÿ ?¿ð*°*ðZB ð sð*¿ÀË1ÿ ?¿ð ° ð`B ð! ð0¿ÀËo×ÿ ?¿ð°ð`B ð" ð0¿ÀËo×ÿ ?¿ððZB ð# sð*¿ÀË1ÿ ?¿ð ðZB ð$ sð*¿ÀË1ÿ ?¿ð°°ðZB ð% sð*¿ÀË1ÿ ?¿ðð ð ðZB ð& sð*¿ÀË1ÿ ?¿ðÀÀð`B ð' ð0¿ÀËo×ÿ ?¿ð°°ðZB ð( sð*¿ÀË1ÿ ?¿ð ðH ð ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²îï ùPç ð`ðð0ð( ð ððx ð cð$`¿ÿ ðÀ°Ððà ð ðx ð cð$¿ÿ ðð°Ððà ð ðH ð ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²îï ùPÿÿÿ ðPðð0ð( ð ððx ð cð$ð¿ÿ ðÀ°Ððà ð ðx ð cð$¬¿ÿ ð °0ðà ð ðH ð ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²îï ù@ÿÿÿ ð@ð´ð0ð( ð ð´ðx ð´ cð$ð¿ÿ ðÀ°Ððà ð ðx ð´ cð$¬¿ÿ ðð°Ððà ð ðH ð´ ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²îï 'ùPÿÿÿ !ð ð&9¤ð±ð( ð ð¤ðÍ ð¤ ð0lÊr¿Àÿ ð°°Ð0 ðm¨cSubtyping: t@ < t* but t@@ < t*@ but Downcast via run-time check, often avoided via flow analysis¡¶! 2 2(2 2=! 2=ª>¦øØÔÐðð~ ð¤ sð*(Ër¿ÿ ðÀ°Ððà r ð ððn ð @P ð¤#ð #"ñ ÃQðð @Àðä 𤠣ð<Ôr¿¿Àÿ?ðÑ@P ðp¨pointer to a t value¡* ¦ø @`ðÖ ð¤ £ð<ØÛr¿¿Àÿ?ð ÑP ðb¨t@¡.¦ø @`ðø 𤠣ð<äàr¿¿Àÿ?ð@Ñ ð¨pointer to a t value or NULL¡6 ¦ø @`ðÖ ð¤ £ð<0ër¿¿Àÿ?ð Ñ ðb¨t*¡.¦ø @`ð`B ð ¤ ð0¿ÀËo×ÿ ?¿ð @ðZB ð ¤ sð*¿ÀË1ÿ ?¿ð Ñ@Ñð`B ð¤ ð0¿ÀËo×ÿ ?¿ð P @P ð`B ð ¤ ð0¿ÀËo×ÿ ?¿ð P ðZB ð ¤ sð*¿ÀË1ÿ ?¿ðP ð`B ð¤ ð0¿ÀËo×ÿ ?¿ð@@P ð± ð¤ ð64îr
ÿÿ¿Àÿð0 à` ð ðK¨<¡ª ð^ ð¤ ð6
¿ÀË>ÿðÀ p` ðXB ð¤ ð0D¿ÀËÑVÑÿð à ð^ ð¤ ð6
¿ÀË>ÿðÀ àÐ ð¢ ð¤ ð0ðr¿¿Àÿð àа ð1¨v¡ 2ð^ ð¤ ð6
¿ÀË>ÿðÐp` ð^B ð ¤ ð6D¿ÀËÑVÎÑÿð0 à0 ð^ ð!¤ ð6
¿ÀË>ÿðÐàÐ ð¢ ð"¤ ð0\ôr¿¿Àÿð àÐÀ ð1¨v¡ 2ð·¢ ð$¤ £ð<ô÷r
¿¿ÀÿðX × ðK¨/¡ª ð± ð%¤ ð6¬ûr
ÿÿ¿Àÿð0 Pð ðK¨<¡ª ð^ ð&¤ ð6
¿ÀË>ÿðÀ `P ð^ ð(¤ ð6
¿ÀË>ÿðÀ ÐÀ ð¢ ð)¤ ð0ðs¿¿Àÿð ÐÀ° ð1¨v¡ 2ð^ ð.¤ ð6
¿ÀË>ÿðÀ ðXB ð/¤ ð0D¿ÀËÑVÑÿð ` ðXB ð2¤ ð0D¿ÀËÑVÑÿð ðÐ ð·¢ ð3¤ £ð<\s
¿¿Àÿðu ¡S¼ ðK¨/¡ª ð^ ð4¤ ð6
¿ÀË>ÿð `P` ð^ ð5¤ ð6
¿ÀË>ÿð ÐÀ` ð¢ ð6¤ ð04 s¿¿ÀÿðpÐÀ ð1¨v¡ 2ð^ ð7¤ ð6
¿ÀË>ÿð ` ðXB ð8¤ ð0D¿ÀËÑVÑÿð ` ð^B ð9¤ ð6D¿ÀËÑVÎÑÿð ðÐ ðH ð¤ ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²îtï ùPç ð0ð¬ðð( ð ð¬ð~ ð¬ sð*ä¿ÿ ðÀ°Ððà ð ð~ ð¬ sð*Të¿ÿ ðð@`ðà ð ðX ð¬ ð0
¿Àÿð`@°ÐðH ð¬ ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²î<ï ùPÿÿÿ ÔðÌ ð°ðdð( ð ð°ð~ ð° sð*ôÕ¿ÿ ðÀ°Ððà ð ð ð° £ð<°Ö¿ÀÄË1ÿ ððààbðà ð ð¢ ð° ð0@Ü¿¿Àÿðp°Ð ð® z Richer types make interface stricter Stricter interface make implementation easier/faster Exposing checks to user lets them optimize Can t check everything statically (e.g., close-once)¡¾ 2¾ðH ð° ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²î<ï ùPÿÿÿ ððøð$ð( ð ðøðr ðø Sð4ÿÿ ðÀ°Ððà ð ðr ðø Sððÿÿ ðð°Ððà ð ðH ðø ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²80º___PPT10ë.âñÄ0¼A#î®ï ùPÿÿÿ ðþð 0ðð( ð ð0ðr ð0 S𤤿ÿ ðÀ°Ððà ð ð7 ð0 ð6Ø¥¿¿ÀÿððàÐ ðѨWvoid f(int*@p) { if(*p != NULL) { g(); **p = 42;//inserted check even w/o g() } }¡2XþRª$Kð ð0 £ð<´«¿Àÿ ð Ppððà ð ð¨ ð 0 ð6¯
ÿÿ¿Àÿðð À` ðB¡ª ð^ ð0 ð6
¿ÀË>ÿðÐÀ@ð^ ð 0 ð6
¿ÀË>ÿð@0@𮢠ð 0 ð0D¹¿¿ÀÿðP@`J ðN¨37¡ 2ªð^ ð0 ð6
¿ÀË>ÿð @ðXB ð0 ð0D¿ÀËÑVÑÿðàð Ðàð^B ð0 ð6D¿ÀËÑVÎÑÿðà`@à悁ð0 £ð<4.q
¿¿Àÿð` 4 0 ðC¨p¡ª ðH ð0 ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²80º___PPT10ë.õÄS¼Sîh ï ùPç Àð¸ðð4ðPð( ð ð4ðx ð4 cð$¿ÿ ðÀ°Ððà ð ðh ð4 ð6¿¿ÀÿððàÐt ð¨Rvoid f(int**p) { int* x = *p; if(x != NULL) { g(); *x = 42;//no check } }¡NSþþ;ª>/ð ð4 £ð<°¿Àÿ ð Ppððà ð ð¨ ð4 ð6ô
ÿÿ¿ÀÿðP Àp ðB¡ª ð^ ð4 ð6
¿ÀË>ÿðàÐÀ ð^ ð4 ð6
¿ÀË>ÿðà@0 𮢠ð 4 ð0Pæq¿¿Àÿð°@`ª ðN¨37¡ 2ªð^ ð 4 ð6
¿ÀË>ÿðà ðXB ð4 ð0D¿ÀËÑVÑÿð@ð ÐAð^B ð 4 ð6D¿ÀËÑVÎÑÿð@`@A悁ð 4 £ð<¬Cq
¿¿Àÿðp` 4 ðC¨p¡ª ð^ ð4 ð6
¿ÀË>ÿðÐÀPð^B ð4 ð6D¿ÀËÑVÎÑÿðÐ`@ñ悁ð4 £ð<7q
¿¿Àÿð pD@ ðC¨x¡ª ðH ð4 ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²80º___PPT10ë.õÄS¼Sîï ù@ÿÿÿ ðàð,ð0ð( ð ð,ðx ð, cð$du¿ÿ ðÀ°Ððà ð ðx ð, cð$ v¿ÿ ðð°Ððà ð ðH ð, ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²îKï ù@ÿÿÿ ãðÛÐð¼ðsð( ð ð¼ð~ ð¼ sð*°a¿ÿ ðÀ°Ððà ð ðx ð¼ cð$lb¿ÿ ð P ðà ð ðRB ð¼ sð*D¿ÀËÔÿð pð¢ ð¼ ð0Te¿¿ÀÿðÀPà ð:¡ 2ª ð¢ ð¼ ð0h¿¿ÀÿðÀ°à ð:¡ 2ª ð¢ ð¼ £ð<°Qq
¿¿ÀÿðP ð+¨©struct Lst<`a> { `a hd; struct Lst<`a>* tl; }; struct Lst<`b>* map( `b f(`a), struct Lst<`a> *); struct Lst<`a>* append( struct Lst<`a>*, struct Lst<`a>*);¡fª ÿ3þÿ3þÿ3þÿ3þþÿ3þÿ3þÿ3þÿ3þþÿ3þÿ3þðH ð¼ ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²î$ï (ù@ç ¼ð´ÀðÀðLð( ð ðÀð~ ðÀ sð*_¿ÿ ðÀ°Ððà ð ð ðÀ cð$pNq¿ÿ ð°àðà ð"¦8¹+sðH ðÀ ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²îï ù@ÿÿÿ ¬ð¤°ðÈð<ð( ð ðÈð~ ðÈ sð*,3¿ÿ ðÀ°Ððà ð ð~ ðÈ sð*Ô3¿ÿ ðð°Ððà ð ðH ðÈ ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²î"ï ù@ÿÿÿ ºð² ð""Üðð( ð ðÜð~ ðÜ sð*¬8¿ÿ ðÀ°Ððà ð ð~ ðÜ sð*h9¿ÿ ððPðà ð ðX ðÜ ð0
ÿÿ¿ÀÿðÐpP ð^2 ðÜ ð6
¿ÀËÑVÿðÀPPðR ðÜ sð*
¿ÀÿðP°pðÒ ðÜ ãðªB(C8DEÁ4FÁ¿ÀËjJÿ ðÿ(Èà8h(8h8pÀè0ø8 @ ¬ðxX°ðRB ðÜ sð*D¿ÀÑÿð°PàðX ð Ü ð0
¿Àÿð°pðX ð Ü ð0
¿Àÿðp@ ÐðX ðÜ ð0
¿Àÿðà0@ð^2 ð Ü ð6
¿ÀËÑVÿððPPÀ ðR ð Ü sð*
¿Àÿð@P° ðÒ ðÜ ãðªB(C8DEÁ4FÁ¿ÀËjJÿ ðÿ(Èà8h(8h8pÀè0ø8 @ ¬ð¨XàðRB ðÜ sð*D¿ÀÑÿðàPðX ðÜ ð0
¿Àÿðàp@ðX ðÜ ð0
¿Àÿð @ ðX ðÜ ð0
¿Àÿðp0Ðð^2 ðÜ ð6
¿ÀËÑVÿð PPð ðR ðÜ sð*
¿ÀÿðpP°ÐðÒ ðÜ ãðªB(C8DEÁ4FÁ¿ÀËjJÿ ðÿ(Èà8h(8h8pÀè0ø8 @ ¬ðØ X ðRB ðÜ sð*D¿ÀÑÿðP@ðX ðÜ ð0
¿ÀÿðppðX ðÜ ð0
¿ÀÿðÐ@ 0 ðX ðÜ ð0
¿Àÿð@ ðX ðÜ ð0
¿Àÿð Ð0ðX ðÜ ð0
¿Àÿð° `ÀðX ðÜ ð0
¿Àÿð ð` ð¾ ðÜ ðBðC@DEÁFÁ¿ÀËjJÐÑÿðÿ@xHðPðpð(h@ ¬ðÐðàð^B ðÜ ð6D¿ÀËjJÐÑÿð0``ð^B ðÜ ð6D¿ÀËjJÐÑÿð0 `` ðÐ2 ð Ü@ ð¨
BÀ¨CÀ¨EÁ$H>lÿI`TQÁ¿ÀËjJÑÿ ðÿÀ¨À¨`T \'À¨À¨`T \'`T`T`T \'`T`Tððp!ðÐ2 ð!Ü@ ð¨
BÀ¨CÀ¨EÁ$H>lÿI`TQÁ¿ÀËjJÑÿ ðÿÀ¨À¨`T \'À¨À¨`T \'`T`T`T \'`T`Tð p!ÈðÐ2 ð"Ü@ ð¨
BÀ¨CÀ¨EÁ$H>lÿI`TQÁ¿ÀËjJÑÿ ðÿÀ¨À¨`T \'À¨À¨`T \'`T`T`T \'`T`TðP p!ø ðH ðÜ ð0Þ½h¿ÿ ??ð0ð Üð!Üð"Üð ÿÿÿÌ33ÌÌÌÿ²²²îï ù@ç ¬ð¤ðàð<ð( ð ðàð~ ðà sð*l+¿ÿ ðÀ°Ððà ð ð~ ðà sð*¸¿ÿ ðð°Ððà ð ðH ðà ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²îÃï ù@ÿÿÿ [ðSðäðëð( ð ðäð~ ðä sð* ¿ÿ ðÀ°Ððà ð ð~ ðä sð*È¿ÿ ðàTðà ð ð§¢ ðä ð0Ü¿¿Àÿð ððà ðG¨void f() { int* x; { int y = 0; x = &y; // x not dangling } // x dangling { int* z = NULL; *x = 123; ... } } ¡Z5&ªðH ðä ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²îï ù@ÿÿÿ ¦ðpðèð6ð( ð ðèð~ ðè sð*ð¿ÿ ðÀ°Ððà ð ðx ðè cð$¬¿ÿ ð°`ðà ð ðH ðè ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²îï ù@ÿÿÿ ¦ð`ðìð6ð( ð ðìð~ ðì sð*pá¿ÿ ðÀ°Ððà ð ðx ðì cð$,â¿ÿ ðð`ðà ð ðH ðì ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²î/ï ù@ÿÿÿ Çð¿PðððWð( ð ðððX ðð ð0
ÿÿ¿Àÿð@Pð~ ðð sð*üË¿ÿ ðÀ°Ððà ð ð~ ðð sð*¸Ì¿ÿ ðð°Ð0 ðà ð ðx2 ðð ³ðB
¿¿ Àÿ?"ñ¿ðÀ `P ð2 ðð ãðT
¿¿ ÀËjJÿ??"ñ¿ðÑm] að~2 ðð ÃðH
¿¿ ÀËjJÿ?"ñ¿ð à Ð0ð ðð ãðT
¿¿ ÀËjJÿ?¿ÿ"ñ¿ðð ° ð ðð ãðT
¿¿ ÀËjJÿ?¿ÿ"ñ¿ðð ° `ð ð ð ãðT
¿¿ ÀËjJÿ?¿ÿ"ñ¿ð P @ð ð ð ãðT
¿¿ ÀËjJÿ?¿ÿ"ñ¿ð °@ð ðð ãðT
¿¿ ÀËjJÿ?¿ÿ"ñ¿ð @À ð ð ð ãðT
¿¿ ÀËjJÿ?¿ÿ"ñ¿ð @ðÀ ð ð ð ãðT
¿¿ ÀËjJÿ?¿ÿ"ñ¿ð Àp@ðÌ¢ ðð óðZÀÓ
¿¿ ÀËjJÿ?¿ÿ"ñ¿ð0 ðJP ð4¨10¡ð ðð ãðT
¿¿ ÀËjJÿ?¿ÿ"ñ¿ð@ À`ðÌ¢ ðð óðZ¸×
¿¿ ÀËjJÿ?¿ÿ"ñ¿ðP @p ð4¨81¡ð ðð ãðT
¿¿ ÀËjJÿ?¿ÿ"ñ¿ðÀ Ðà ðÌ¢ ðð óðZÛ
¿¿ ÀËjJÿ?¿ÿ"ñ¿ðÐPªð ð4¨11¡ðB ðð@ ÓðN¿D¿ÀËjJÑÿ?¿ÿ"ñ¿ð pÀ ðB ðð@ ÓðN¿D¿ÀËjJÑÿ?¿ÿ"ñ¿ð ÐðB ðð@ ÓðN¿D¿ÀËjJÑÿ?¿ÿ"ñ¿ð0 0 ðÁ¢ ðð ÓðNÌ)r¿¿ ÀËjJÿ?¿ÿ"ñ¿ð `°@ ð5¨0¡ 2ðB ðð@ ÓðN¿D¿ÀËjJÑÿ?¿ÿ"ñ¿ð0 ÐP 1 ðB ðð@ ÓðN¿D¿ÀËjJÑÿ?¿ÿ"ñ¿ð° Àà à ðH ðð ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²î ï ù@ç ¸ð°@ðôðHð( ð ðôð~ ðô sð*³¿ÿ ðÀ°Ððà ð ð ðô ð6ø¿¿ÀÄÿ ðð°Ððà ð ðH ðô ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²î<ï ùPÿÿÿ ð0ðüð$ð( ð ðüðr ðü Sð¨¿ÿ ðÀ°Ððà ð ðr ðü Sð|®¿ÿ ð°Ð ðà ð ðH ðü ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²80º___PPT10ë.âñİ4îï ù@ÿÿÿ ð ðð0ð( ð ððx ð cð$ ¿ÿ ðÀ°Ððà ð ðx ð cð$H¡¿ÿ ðð°Ððà ð ðH ð ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²î<ï ùPÿÿÿ ððð$ð( ð ððr ð Sðä¿ÿ ðÀ°Ððà ð ðr ð Sð ¿ÿ ðð°`ðà ð ðH ð ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²80º___PPT10ë.âñÄ0ÖjSî<ï ùPÿÿÿ ððð$ð( ð ððr ð SðT
¿ÿ ðÀ°Ððà ð ðr ð Sð¿ÿ ðð°Ððà ð ðH ð ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²80º___PPT10ë.âñÄèî<ï ùPÿÿÿ ððð ð$ð( ð ð ðr ð Sð¬}¿ÿ ðÀ°Ððà ð ðr ð Sðh~¿ÿ ðð°0ðà ð ðH ð ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²80º___PPT10ë.ãñļ!îï ùPÿÿÿ ðàðð0ð( ð ððx ð cð$Ôk¿ÿ ðÀ°Ððà ð ðx ð cð$l¿ÿ ðð°`ðà ð ðH ð ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²î<ï ùPÿÿÿ ðÐð ð$ð( ð ð ðr ð Sð´\¿ÿ ðÀ°Ððà ð ðr ð Sðp]¿ÿ ðð°Ððà ð ðH ð ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²80º___PPT10ë.óñÄ`Ö¦Áîï ù@ç ðÀð(ð0ð( ð ð(ðx ð( cð$ÄH¿ÿ ðÀ°Ððà ð ðx ð( cð$I¿ÿ ðð°0ðà ð ðH ð( ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²î<ï ùPÿÿÿ ð°ðð$ð( ð ððr ð SðàB¿ÿ ðÀ°Ððà ð ðr ð SðC¿ÿ ðð°Ððà ð ðH ð ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²80º___PPT10ë.áñİÓîNï ùPÿÿÿ ¦ð ðð6ð( ð ððr ð SðÀ,¿ÿ ðÀ°Ððà ð ð ð Sð¤9¿ÿ ðð°Ððà ð¦ ÙÕ!ðH ð ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²80º___PPT10ë.óñÄP©_Pîï ùPÿÿÿ ððð0ð( ð ððx ð cð$\'¿ÿ ðÀ°Ððà ð ðx ð cð$(¿ÿ ðð°Ððà ð ðH ð ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²îï ùPÿÿÿ ðð ð0ð( ð ð ðx ð cð$¿ÿ ðÀ°Ððà ð ðx ð cð$À¿ÿ ðð°Ððà ð ðH ð ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²îï ù@ÿÿÿ ®ð¦pð8ð>ð( ð ð8ðx ð8 cð$ ¿ÿ ðÀ°Ððà ð ð ð8 cð$¿ÿ ðð°Ððà ð¦ ðH ð8 ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²ðØñ 0 ðPðxð(ð( ð ðxð^ ðx Sð¿ÿ0ð·æRH ðÃsð ðx cð$µs¿ÿ0ðÚ Lì!ðà s ðª ðH ðx ð0ßjBÁ¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²ðäñ 0 ¤ððXð4ð( ð ðXðd ðX cð$¿ÿ0ð·æRH ðÃ{ð ðX sð* 7{¿ÿ0ðÚ Lì!ðà { ðª ðH ðX ð0ßjBÁ¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²ðäñ 0 ¤ð0ðð4ð( ð ððd ð cð$¿ÿ0ð·æRH ðÃ{ð ð sð*ì {¿ÿ0ðÚ Lì!ðà { ðª ðH ð ð0ßjBÁ¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²ðFñ 0 ðþPð¨ðð( ð ð¨ðd ð¨ cð$¿ÿ0ð·æRH ðÃðò ð¨ 3ðr¬Ö²eÙ²²eÙ²
¿¿ÿ0ðÚ Lì!ðà ð8¨$EXAMPLE OF SUBTYPING AS BACKUP SLIDEðH ð¨ ð0ßjBÁ¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²ð,ñ 0 ìðä`ðÄð|ð( ð ðÄðd ðÄ cð$¿ÿ0ð·æRH ðÃðØ ðÄ 3ðr¼ô²eÙ²²eÙ²
¿¿ÿ0ðÚ Lì!ðà ðª ðH ðÄ ð0ßjBÁ¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²ðäñ' 0 ¤ð ðð4ð( ð ððd ð cð$¿ÿ0ð·æRH ðÃ{ð ð sð*Ì<{¿ÿ0ðÚ Lì!ðà { ðª ðH ð ð0ßjBÁ¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²røP Ö¦§^y¢Â ¡©¿«Åd{Çï±ÿ³¶¸EºBÒöíðHhP}¬nò&ô· 3 wØÐñ%D,p.0¶AÒCG³IÉK[(]l_|aÀcFsVu<fÏ߯Xjðp¾lá#»qfwõíª
ôCèFé(à8Ø òú/È 0ÒÕ0·DTimes New Roman©Ñ´ÕÕì 0´ÕWo 0·DArialNew Roman©Ñ´ÕÕì 0´ÕWo 0" ·DCourier Newman©Ñ´ÕÕì 0.Times New RomanArial Courier New Wingdingsdan_design_template5Cyclone: A Memory-Safe C-Level Programming Language A safe C-level languageCallers problem?Safe low-level systemsSome insufficient approachesCyclone in briefThe plan from hereStatusEvaluationCode differencesRun-time performanceLarger program: the compilerOther projectsThe plan from hereNot-null pointersExampleA classic moral Key Design Principles in ActionIts always aliasingIts always aliasingThe plan from hereChange void* to `aNot much new hereExistential typesRegionsCyclone regions [PLDI 02]Thats the easy partThe big restrictionRegion polymorphismType definitionsRegion subtypingRegions evaluationThe plan from hereOther safety holesAnd modern conveniencesPlenty of work remainsRelated work: making C saferRelated Work: Checking C codeRelated work: higher and lowerSummary Availability Fonts UsedDesign Template Slide Titles)sign Templateö$_ÀãÜÈ ôyDan GrossmanDan Grossman$_Àãļ ôÑDan GrossmanDan Grossman Memory ##. Ìf. 2 ×-. Ìf.2 ×wman©Ñ´ÕÕì 0´ÕWo 010·DWingdingswman©Ñ´ÕÕì 0´ÕWo 0¤ `ÿÿÿÿ¥ .© @£nÿý?" dd@ÿÿïÿÿÿÿÿÿ @@`` ðüð@~6/ /7ZM)@280c //2 0/,+*)($3')&% :4"$3#!.2- ð0A¿ÀÅAÿpñÿ3ÌfÌfÿÿÿfÿ@ñ÷ð8óóÐÑððnÊ;ÇÊ;úgþý4XdXdì 0¨Õÿÿÿ¦ÿÿÿpûppû@<ý4!d!d® 0dÙªÑ<ý4dddd® 0dÙªÑ<ý4BdBd® 0dÙªÑÿ N0º___PPT10 ÀÀº___PPT9ð®è¯¬`ÿÿÿÿÿÿ¯¬Xÿÿ?ÙdÚ-º11 January 2005 º*Dan Grossman: CycloneOÙ Ú=ð{ó¨4Cyclone: A Memory-Safe C-Level Programming Language ¡"53 Ìfþ¨¬Dan Grossman University of Washington Joint work with: Trevor Jim AT&T Research Greg Morrisett Harvard University Michael Hicks University of Maryland¡:'(&Ìfþó¨A safe C-level language¨ Cyclone is a programming language and compiler aimed at safe systems programming C is not memory safe: void f(int* p, int i, int v) { p[i] = v; } Address p+i might hold important data or code Memory safety is crucial for reasoning about programs ¡S9h:ÿ3þÿ3þ þþþþ $ 6óà "Caller s problem?ª¨Ã void g(void**, void*); int y = 0; int *z = &y; g(&z,0xBAD); *z = 123; Might be safe, but not if g does *x=y Type of g enough for code generation Type of g not enough for safety checking¡$N v þþ þ!%ª> s& óë'¨Safe low-level systems¨8For a safety guarantee today, use YFHLL Your Favorite High Level Language YFHLL provides safety in part via: hidden data fields and run-time checks automatic memory management Data representation and resource management are essential aspects of low-level systems There are strong reasons for C-like languages¡(##D$Y.(ÌfþÌfþÌfþÌfþÌfþ#ÿ3þ! ÿ3þ0 ÿ3þ-óì(¨Some insufficient approaches ®Compile C with extra information type fields, size fields, live-pointer table, & treats C as a higher-level language Use static analysis very difficult less modular Ban unsafe features there are many you need them¡!U!T óǨCyclone in brief *A safe, convenient, and modern language at the C level of abstraction Safe: memory safety, abstract types, no core dumps C-level: user-controlled data representation and resource management, easy interoperability, manifest cost Convenient: may need more type annotations, but work hard to avoid it Modern: add features to capture common idioms New code for legacy or inherently low-level systems ¡ôGZZ6ZZFÿþÿþ. e ; '6óȨThe plan from here êExperience with Cyclone Benchmarks, ports, systems, compiler, & All on Earth so far Jð Not-NULL pointers Type-variable examples generics region-based memory management Brief view of everything else Related work Really just a taste of Cyclone¡ÂZ>Z)Z(Z-Z"Z< (-"óɨStatus ® Cyclone really exists (except memory-safe threads) >150K lines of Cyclone code, including the compiler gcc back-end (Linux, Cygwin, OSX, Mindstorm, & ) User s manual, mailing lists, & Still a research vehicle ¡À4¢34 0 ª ?óʨ Evaluation¨æ Is Cyclone like C? port code, measure source differences interface with C code (extend systems) What is the performance cost? port code, measure slowdown Is Cyclone good for low-level systems? write systems, ensure scalability ¡Ê" N" '" "N '"óË ¨Code differences¨Porting not automatic, but quite similar Many changes identify arrays and lengths Some changes incidental (absent prototypes, new keywords)¡óÌ ¨Run-time performance¨ÐRHLinux 7.1 (2.4.9), 1.0GHz PIII, 512MRAM, gcc2.96 -O3, glibc 2.2.4 Comparable to other safe languages to start C level provides important optimization opportunities Understanding the applications could help¡LED,6*óͨLarger !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~
¡¢£¤¥¦§¨©ª«¬®¯°±²³´µ¶·¸¹º»¼½¾¿ÀÁÂÃàÅÆþÿÿÿÈÉÊËÌÍÎÏÐÑÒÓÔÕÖרÙÚÛ=ýÿÿÿýÿÿÿßþÿÿÿáâãäåæçèéêëìíîïðñòóôõö÷øùúûüýþÿRoot EntryÿÿÿÿÿÿÿÿdOÏꪹ)è ÖÛìÑøÄ6@Current UserÿÿÿÿÿÿÿÿÿÿÿÿKDSummaryInformation(ÿÿÿÿÿÿÿÿ PowerPoint Document(ÿÿÿÿÉDocumentSummaryInformation8ÿÿÿÿÿÿÿÿÿÿÿÿ3èÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿ´ÕWo 010·DWingdingswman©Ñ´ÕÕì 0´ÕWo 0¤ `ÿÿÿÿ¥ .© @£nÿý?" dd@ÿÿïÿÿÿÿÿÿ @@`` ðüð@~6/ /7ZM)@280c //2 0/,+*)($3')&% :4"$3#!.2- ð0A¿ÀÅAÿpñÿ3ÌfÌfÿÿÿfÿ@ñ÷ð8óóÐÑððnÊ;ÇÊ;úgþý4XdXdì 0¨Õÿÿÿ¦ÿÿÿpûppû@<ý4!d!d® 0dÙªÑ<ý4dddd® 0dÙªÑ<ý4BdBd® 0dÙªÑÿ N0º___PPT10 ÀÀº___PPT9ð®è¯¬`ÿÿÿÿÿÿ¯¬Xÿÿ?ÙdÚ-º11 January 2005 º*Dan Grossman: CycloneOÙ Ú=ðW{ó¨4Cyclone: A Memory-Safe C-Level Programming Language ¡"53 Ìfþ¨¬Dan Grossman University of Washington Joint work with: Trevor Jim AT&T Research Greg Morrisett Harvard University Michael Hicks University of Maryland¡:'(&Ìfþó¨A safe C-level language¨ Cyclone is a programming language and compiler aimed at safe systems programming C is not memory safe: void f(int* p, int i, int v) { p[i] = v; } Address p+i might hold important data or code Memory safety is crucial for reasoning about programs ¡S9h:ÿ3þÿ3þ þþþþ $ 6óà "Caller s problem?ª¨Ã void g(void**, void*); int y = 0; int *z = &y; g(&z,0xBAD); *z = 123; Might be safe, but not if g does *x=y Type of g enough for code generation Type of g not enough for safety checking¡$N v þþ þ!%ª> s& óë'¨Safe low-level systems¨8For a safety guarantee today, use YFHLL Your Favorite High Level Language YFHLL provides safety in part via: hidden data fields and run-time checks automatic memory management Data representation and resource management are essential aspects of low-level systems There are strong reasons for C-like languages¡(##D$Y.(ÌfþÌfþÌfþÌfþÌfþ#ÿ3þ! ÿ3þ0 ÿ3þ-óì(¨Some insufficient approaches ®Compile C with extra information type fields, size fields, live-pointer table, & treats C as a higher-level language Use static analysis very difficult less modular Ban unsafe features there are many you need them¡!U!T óǨCyclone in brief *A safe, convenient, and modern language at the C level of abstraction Safe: memory safety, abstract types, no core dumps C-level: user-controlled data representation and resource management, easy interoperability, manifest cost Convenient: may need more type annotations, but work hard to avoid it Modern: add features to capture common idioms New code for legacy or inherently low-level systems ¡ôGZZ6ZZFÿþÿþ. e ; '6óȨThe plan from here êExperience with Cyclone Benchmarks, ports, systems, compiler, & All on Earth so far Jð Not-NULL pointers Type-variable examples generics region-based memory management Brief view of everything else Related work Really just a taste of Cyclone¡ÂZ>Z)Z(Z-Z"Z< (-"óɨStatus ® Cyclone really exists (except memory-safe threads) >150K lines of Cyclone code, including the compiler gcc back-end (Linux, Cygwin, OSX, Mindstorm, & ) User s manual, mailing lists, & Still a research vehicle ¡À4¢34 0 ª ?óʨ Evaluation¨æ Is Cyclone like C? port code, measure source differences interface with C code (extend systems) What is the performance cost? port code, measure slowdown Is Cyclone good for low-level systems? write systems, ensure scalability ¡Ê" N" '" "N '"óË ¨Code differences¨Porting not automatic, but quite similar Many changes identify arrays and lengths Some changes incidental (absent prototypes, new keywords)¡óÌ ¨Run-time performance¨ÐRHLinux 7.1 (2.4.9), 1.0GHz PIII, 512MRAM, gcc2.96 -O3, glibc 2.2.4 Comparable to other safe languages to start C level provides important optimization opportunities Understanding the applications could help¡LED,6*óͨLarger program: the compiler¨Ö Scalable compiler + libraries (80K lines) build in < 30secs Generic libraries (e.g., lists, hashtables) clients have no syntactic/performance cost Static safety helps exploit the C-level I use &x more than in C ¡¼ 4,,( 3 ,+ ( óÎ ¨Other projects¨oOpen Kernel Environment [Bos/Samwel, OPENARCH 02] MediaNet [Hicks et al, OPENARCH 03]: RBClick [Patel/Lepreau, OPENARCH 03] STP [Patel et al., SOSP 03] FPGA synthesis [Teifel/Manohar, ISACS 04] Maryland undergrad O/S course (geekOS) [2004] Windows device driver (6K lines) Only 100 lines left in C But unrecoverable failures & other kernel corruptions remain ¡PWPP ' !Wªt =,óÒ¨The plan from here ,Experience with Cyclone Not-NULL pointers Type-variable examples generics region-based memory management Brief view of everything else Related work ¡zA(-(-óÓ¨Not-null pointersª óÔ¨Example êFILE* fopen(const char@, const char@); int fgetc(FILE@); int fclose(FILE@); void g() { FILE* f = fopen( foo , r ); int c; while((c = fgetc(f)) != EOF) {& } fclose(f); } Gives warning and inserts one null-check Encourages a hoisted check¡Ü±ZEZþ þ þþ þQDª aóÕ¨A classic moral¨LFILE* fopen(const char@, const char@); int fgetc(FILE@); int fclose(FILE@); ¡Mþ þ þ ª,1 óÖ!¨Key Design Principles in Action¨KTypes to express invariants Preconditions for arguments Properties of values in memory Flow analysis where helpful Lets users control explicit checks Soundness + aliasing limits usefulness Users control data representation Pointers are addresses unless user allows otherwise Often can interoperate with C more safely just via types¡°Z;ZZJZ"Z4Z9Z;#'"49ª$Rñóò. (It s always aliasing¨¿But can avoid checks when compiler knows all aliases. Can know by: Types: precondition checked at call site Flow: new objects start unaliased Else user should use a temporary (the safe thing)¡ C}Àª 3óó/ (It s always aliasing¨¿But can avoid checks when compiler knows all aliases. Can know by: Types: precondition checked at call site Flow: new objects start unaliased Else user should use a temporary (the safe thing)¡ C}Àª 3óñ-¨The plan from here ,Experience with Cyclone Not-NULL pointers Type-variable examples generics region-based memory management Brief view of everything else Related work ¡pA(-*(-óØ ( Change void* to `a ¡:¨struct Lst { void* hd; struct Lst* tl; }; struct Lst* map( void* f(void*), struct Lst*); struct Lst* append( struct Lst*, struct Lst*);¡\ ;þ1þ!óÙ¨Not much new here¨Closer to C than C++, Java generics, ML, etc. Unlike funcýÿÿÿ !"#$%&'()*+,-./01234Çþÿÿÿ789:;<Ä>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ýÿÿÿtional languages, data representation may restrict `a to pointers, int why not structs? why not float? why int? Unlike templates, no code duplication or leaking implementations Unlike objects, no need to tag data¡Ú/S)f/"N"c""c"c" " f"ª¦ióÚ¨Existential types Programs need a way for call-back types: struct T { void (*f)(void*, int); void* env; }; We use an existential type (simplified): struct T { <`a> void (@f)(`a, int); `a env; }; more C-level than baked-in closures/objects ¡+ZA0ZZ*ZA0Z,8ZZ+>" ÿþgÿþGÿþgÿ3þ gÿ3þ, "óÛ¨Regions a.k.a. zones, arenas, & Every object is in exactly one region Allocation via a region handle Deallocate an entire region simultaneously (cannot free an object) Old idea with recent support in languages (e.g., RC, RTSJ) and implementations (e.g., ML Kit)¡²|Z*ZZ_Z&7 _ª>`F. %óܨCyclone regions [PLDI 02]¡ heap region: one, lives forever, conservatively GC d stack regions: correspond to local-declaration blocks: {int x; int y; s} growable regions: scoped lifetime, but growable: {region r; s} allocation routines take a region handle handles are first-class caller decides where, callee decides how much no handles for stack regions¡m4B K (*þþ#þ".ÿ3þªb,1\óÝ (That s the easy part¨cThe implementation is really simple because the type system statically prevents dangling pointers ¡hd ÿþóÞ¨The big restriction ÎAnnotate all pointer types with a region name (a type variable of region kind) int@`r means pointer into the region created by the construct that introduces `r heap introduces `H L:& introduces `L {region r; s} introduces `r r has type region_t<`r> compile-time check: only live regions are accessed by default, function arguments point to live regions ¡PS$B² 35"" GgI"c"bc"c "cgþc "c" " c " c c 3b5bcªP¡''jóߨRegion polymorphism øApply what we did for type variables to region names (only it s more important and could be more onerous) void swap(int @`r1 x, int @`r2 y){ int tmp = *x; *x = *y; *y = tmp; } int@`r sumptr(region_t<`r> r,int x,int y){ return rnew(r) (x+y); }¡BkM EkCGþCgcgþcgcgþ cgþ cCC g ÿþ c g þ c g ÿþ c g þ c g þ c g þ c ª,Óóà¨Type definitions¨Kstruct ILst<`r1,`r2> { int@`r1 hd; struct ILst<`r1,`r2> *`r2 tl; }; ¡ L CgÿþC g ÿþCgÿþCgÿþ C $g$ÿþ(C(,g,ÿþ 0C000óá ¨Region subtyping ÒIf p points to an int in a region with name `r1, is it ever sound to give p type int*`r2? If so, let int*`r1 < int*`r2 Region subtyping is the outlives relationship {region r1; & {region r2; & } & } LIFO makes subtyping common ¡$[M!gÿþ g ÿþ CgÿþoÿþçÿGCgÿþnÿþçÿoÿþçÿ B F B $ C B C ª>ª óâ"¨Regions evaluationª ÆLIFO regions good for some idioms awkward in C Regions generalize stack variables and the heap Defaults and inference make it surprisingly palatable Worst part: defining region-allocated data structures Cyclone actually has much more [ISMM 04] Non-LIFO regions Unique pointers Explicitly reference-counted pointers A unified system , not n sublangages ¡/xf6)p/f6 a ªWóã#¨The plan from here ,Experience with Cyclone Not-NULL pointers Type-variable examples generics region-based memory management Brief view of everything else Related work ¡pA(-A( óä$¨Other safety holes JArrays (what or where is the size) Options: dynamic bound, in a field/variable, compile-time bound, special string support Threads (avoiding races) vaporware type system to enforce lock-based mutual exclusion Casts Allow only up casts and casts to numbers Unions Checked tags or bits-only fields Uninitialized data Flow analysis (safer and easier than default initializers) Varargs (safe via changed calling convention)¡î#X=+!;.#X=+ ! ;.ª> A'óå%¨And modern conveniences æ30 years after C, some things are worth adding& Tagged unions and pattern matching on them Intraprocedural type inference Tuples (like anonymous structs) Exceptions Struct and array initializers Namespaces new for allocation + initialization ¡Z0xÃ0 "ª>{ Hóê&¨Plenty of work remains¨ÓCommon limitations: Aliasing Arithmetic Unportable assumptions (But interoperating with C is much simpler than in a HLL) Big challenge for next generation: guarantees beyond fail-safe (i.e., graceful abort)¡X,:Y^rª( ¢óϨRelated work: making C safer ÊCompile to make dynamic checks possible Safe-C [Austin et al.], RTC [Yong/Horwitz], ... Purify, Stackguard, Electric Fence, & CCured [Necula et al.] performance via whole-program analysis less user burden less memory management, single-threaded Control-C [Adve et al.] weaker guaranty, less burden SFI [Wahbe, Small, ...]: sandboxing via binary rewriting ¡ð(ZmZ`ZpZZ(1` # ª>@aóí*¨Related Work: Checking C code fModel-checking C code (SLAM, BLAST, & ) Leverages scalability of MC Key is automatic building and refining of model They assume (weak) memory safety Lint-like tools (Splint, Metal, PreFIX, & ) Good at reducing false positives Cannot ensure absence of bugs Metal particularly good for user-defined checks Cqual (user-defined qualifiers, lots of inference) Better for unchangeable code or user-defined checks (i.e., they re complementary)¡Â'm+o3S'Q+!H2 Sª,´tóð,¨Related work: higher and lower ¸Adapted/extended ideas: polymorphism [ML, Haskell, & ] regions [Tofte/Talpin, Walker et al., & ] safety via dataflow [Java, & ] existential types [Mitchell/Plotkin, & ] controlling data representation [Ada, Modula-3, & ] Safe lower-level languages [TAL, PCC, & ] engineered for machine-generated code Vault: stronger properties via restricted aliasing ¡Á)'4À)&4óѨSummary òCyclone: a safe language at the C-level of abstraction Synergistic combination of types, flow analysis, and run-time checks A real compiler and prototype applications Properties like not NULL , has longer lifetime , has array length & now in the language and checked Easy interoperability with C allow smooth and incremental move toward memory safety in theory at least¡zg7 E + g Uóî)¨ Availability Like any language, you have to kick the tires : www.research.att.com/projects/cyclone Also see: Jan. 2005 C/C++ User s Journal USENIX 2002 Conversely, I want to know NASA s C-level code needs Maybe ideas from Cyclone will help Maybe not Either way would be fascinating ¡¢1' +5-!1%Ìfþ +ª1Ìóæ¨ r[Presentation ends here some auxiliary slides follow]¡::óç¨Example in Cyclone¨void f(int@{`j} p, tag_t<`i> i, int v ; `i < `j){ p[i] = v; } Note: regions and locks use implicit defaults (live and accessible)¡ÌIEþÿ3þ ÿ3þ ÿ3þFª,"Róô0¨Some other problems \One safety violation typically renders all program properties potentially irrelevant So prohibit: incorrect casts, array-bounds violations, misused unions, uninitialized pointers, dangling pointers, null-pointer dereferences, dangling longjmp, vararg mismatch, not returning pointers, data races, & ¡,dZËZdË/ð¨ó^óÅ%óÐ&óè'óé(óï)Pÿÿÿêîtï ùPØ ð0ð¬ðð( ð ð¬ð~ ð¬ sð*ä¿ÿ ðÀ°Ððà ð ð~ ð¬ sð*Të¿ÿ ðð@`ðà ð ðX ð¬ ð0
¿Àÿð`@°ð ðH ð¬ ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²î<ï ùPÿÿÿ ððøð$ð( ð ðøðr ðø Sð4ÿÿ ðÀ°Ððà ð ðr ðø Sððÿÿ ðð°Ððà ð ðH ðø ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²80º___PPT10ë.âñÄ0¼A#îÊï ùPÿÿÿ "ðð 0ð²ð( ð ð0ðr ð0 S𤤿ÿ ðÀ°Ððà ð ðS ð0 ð6Ø¥¿¿ÀÿððàÐ ðí¨Wvoid f(int*@p) { if(*p != NULL) { g(); **p = 42;//inserted check even w/o g() } }¡NXþþKª$Kð ð0 £ð<´«¿Àÿ ð Ppððà ð ð¨ ð 0 ð6¯
ÿÿ¿Àÿðð À` ðB¡ª ð^ ð0 ð6
¿ÀË>ÿðÐÀ@ð^ ð 0 ð6
¿ÀË>ÿð@0@𮢠ð 0 ð0D¹¿¿ÀÿðP@`J ðN¨37¡ 2ªð^ ð0 ð6
¿ÀË>ÿð @ðXB ð0 ð0D¿ÀËÑVÑÿðàð Ðàð^B ð0 ð6D¿ÀËÑVÎÑÿðà`@à悁ð0 £ð<4.q
¿¿Àÿð` 4 0 ðC¨p¡ª ðH ð0 ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²80º___PPT10ë.õÄS¼Sî ï ùPÿÿÿ ÜðÔðð4ðlð( ð ð4ðx ð4 cð$¿ÿ ðÀ°Ððà ð ð ð4 ð6¿¿ÀÿððàÐt ð¨Rvoid f(int**p) { int* x = *p; if(x != NULL) { g(); *x = 42;//no check } }¡jSþþ þ;ª>/ð ð4 £ð<°¿Àÿ ð Ppððà ð ð¨ ð4 ð6ô
ÿÿ¿ÀÿðP Àp ðB¡ª ð^ ð4 ð6
¿ÀË>ÿðàÐÀ ð^ ð4 ð6
¿ÀË>ÿðà@0 𮢠ð 4 ð0Pæq¿¿Àÿð°@`ª ðN¨37¡ 2ªð^ ð 4 ð6
¿ÀË>ÿðà ðXB ð4 ð0D¿ÀËÑVÑÿð@ð ÐAð^B ð 4 ð6D¿ÀËÑVÎÑÿð@`@A悁ð 4 £ð<¬Cq
¿¿Àÿðp` 4 ðC¨p¡ª ð^ ð4 ð6
¿ÀË>ÿðÐÀPð^B ð4 ð6D¿ÀËÑVÎÑÿðÐ`@ñ悁ð4 £ð<7q
¿¿Àÿð pD@ ðC¨x¡ª ðH ð4 ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²80º___PPT10ë.õÄS¼Sîï ù@ ¬ð¤ðàð<ð( ð ðàð~ ðà sð*l+¿ÿ ðÀ°Ððà ð ð~ ðà sð*¸¿ÿ ðð°Ððà ð ðH ðà ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²î6ï ù@ÿÿÿ ÎðÆðäð^ð( ð ðäð~ ðä sð* ¿ÿ ðÀ°Ððà ð ð~ ðä sð*È¿ÿ ðàTðà ð ð¢ ðä ð0Ü¿¿Àÿð ððà ðº¨void f() { int* x; { int y = 0; x = &y; // x not dangling } // x dangling { int* z = NULL; *x = 123; ... } } ¡øZþ þþ þªðH ðä ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²r0ÎÔÖÜ :(V*ò Ü®õíª.ôCèpé(à8Ø òú/È 0ÒÕ0·DTimes New Roman©Ñ´ÕÕì 0´ÕWo 0·DArialNew Roman©Ñ´ÕÕì 0´ÕWo 0" ·DCourier Ne !"#$%&'()*+,-./012þÿÿÿ456789:;<=>?@ABCDEFGHIJþÿÿÿLþÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿþÿà
òùOh«+'³Ù0\ hp°Èô 8 D P\dä8Cyclone: Safe Programming at the C Level of Abstraction Dan Grossman Pr!T:\talks\dan_design_template.potC L Dan Grossmandes307Microsoft PowerPointemp@0«M@0ÅtÂ@`®ÒìÑøÄGî ÿÿÿÿg o1&ÿÿÿÿÀÐ &ÿÿÿÿ&#ÿÿÿÿTNPP Ñ2ÿÿOMi & TNPPô &ÿÿÿÿ&TNPP ÐÀ üÿÿÿ-ú-- !ðÐÀ-üÿÿÿ-ðú-&ÿÿÿÿM
l-ü33Ì- $PPhh--ð&ÿÿÿÿ&ÿÿÿÿM]ld-ü33Ì- $P^Pbhbh^--ð&ÿÿÿÿü--!y¨H--ûÜñw@± ÜÌñØówáów õw fÍ- ûÕÿ@"Arial- ÊëØówáów õw fÍ-ð Ìf.!2 פCyclone: A Memory ##. Ìf. 2 ×-. Ìf.2 ×&Safe C . Ìf. 2 ש-. Ìf.2 ×·Level . Ìf.%2 ûProgramming Language$# .--ñy88-- Ìfûàÿ@"Arial± çëØówáów õw fÍ-ð Ìf.2 \m Dan Grossman . Ìf.+2 (University of Washington . 33Ì.12 òKJoint work with: Trevor Jim . 33Ì.2 ò" AT&T Research . 33Ì.2 8Greg Morrisett . 33Ì."2 "Harvard University . 33Ì.2 >8 Michael Hicks . 33Ì.(2 >"University of Maryland .--û¼"SystemÍ fÍ !Àõ-ð&TNPP &ÿÿÿÿþÿÕÍÕ.+,ù®0¸¨¸ÀÈÐ Ø àèðø VäOn-screen ShowCUCSreeÉ)í program: the compiler¨Ö Scalable compiler + libraries (80K lines) build in < 30secs Generic libraries (e.g., lists, hashtables) clients have no syntactic/performance cost Static safety helps exploit the C-level I use &x more than in C ¡¼ 4,,( 3 ,+ ( óÎ ¨Other projects¨oOpen Kernel Environment [Bos/Samwel, OPENARCH 02] MediaNet [Hicks et al, OPENARCH 03]: RBClick [Patel/Lepreau, OPENARCH 03] STP [Patel et al., SOSP 03] FPGA synthesis [Teifel/Manohar, ISACS 04] Maryland undergrad O/S course (geekOS) [2004] Windows device driver (6K lines) Only 100 lines left in C But unrecoverable failures & other kernel corruptions remain ¡PWPP ' !Wªt =,óÒ¨The plan from here ,Experience with Cyclone Not-NULL pointers Type-variable examples generics region-based memory management Brief view of everything else Related work ¡zA(-(-óÓ¨Not-null pointersª óÔ¨Example êFILE* fopen(const char@, const char@); int fgetc(FILE@); int fclose(FILE@); void g() { FILE* f = fopen( foo , r ); int c; while((c = fgetc(f)) != EOF) {& } fclose(f); } Gives warning and inserts one null-check Encourages a hoisted check¡Ü±ZEZþ þ þþ þQDª aóÕ¨A classic moral¨LFILE* fopen(const char@, const char@); int fgetc(FILE@); int fclose(FILE@); ¡Mþ þ þ ª,1 óÖ!¨Key Design Principles in Action¨KTypes to express invariants Preconditions for arguments Properties of values in memory Flow analysis where helpful Lets users control explicit checks Soundness + aliasing limits usefulness Users control data representation Pointers are addresses unless user allows otherwise Often can interoperate with C more safely just via types¡°Z;ZZJZ"Z4Z9Z;#'"49ª$Rñóò. (It s always aliasing¨¿But can avoid checks when compiler knows all aliases. Can know by: Types: precondition checked at call site Flow: new objects start unaliased Else user should use a temporary (the safe thing)¡ C}Àª 3óó/ (It s always aliasing¨¿But can avoid checks when compiler knows all aliases. Can know by: Types: precondition checked at call site Flow: new objects start unaliased Else user should use a temporary (the safe thing)¡ C}Àª 3óñ-¨The plan from here ,Experience with Cyclone Not-NULL pointers Type-variable examples generics region-based memory management Brief view of everything else Related work ¡pA(-*(-óØ ( Change void* to `a ¡:¨struct Lst { void* hd; struct Lst* tl; }; struct Lst* map( void* f(void*), struct Lst*); struct Lst* append( struct Lst*, struct Lst*);¡\ ;þ1þ!óÙ¨Not much new here¨Closer to C than C++, Java generics, ML, etc. Unlike functional languages, data representation may restrict `a to pointers, int why not structs? why not float? why int? Unlike templates, no code duplication or leaking implementations Unlike objects, no need to tag data¡Ú/S)f/"N"c""c"c" " f"ª¦ióÚ¨Existential types Programs need a way for call-back types: struct T { void (*f)(void*, int); void* env; }; We use an existential type (simplified): struct T { <`a> void (@f)(`a, int); `a env; }; more C-level than baked-in closures/objects ¡+ZA0ZZ*ZA0Z,8ZZ+>" ÿþgÿþGÿþgÿ3þ gÿ3þ, "óÛ¨Regions a.k.a. zones, arenas, & Every object is in exactly one region Allocation via a region handle Deallocate an entire region simultaneously (cannot free an object) Old idea with recent support in languages (e.g., RC, RTSJ) and implementations (e.g., ML Kit)¡²|Z*ZZ_Z&7 _ª>`F. %óܨCyclone regions [PLDI 02]¡ heap region: one, lives forever, conservatively GC d stack regions: correspond to local-declaration blocks: {int x; int y; s} growable regions: scoped lifetime, but growable: {region r; s} allocation routines take a region handle handles are first-class caller decides where, callee decides how much no handles for stack regions¡m4B K (*þþ#þ".ÿ3þªb,1\óÝ (That s the easy part¨cThe implementation is really simple because the type system statically prevents dangling pointers ¡hd ÿþóÞ¨The big restriction ÎAnnotate all pointer types with a region name (a type variable of region kind) int@`r means pointer into the region created by the construct that introduces `r heap introduces `H L:& introduces `L {region r; s} introduces `r r has type region_t<`r> compile-time check: only live regions are accessed by default, function arguments point to live regions ¡PS$B² 35"" GgI"c"bc"c "cgþc "c" " c " c c 3b5bcªP¡''jóߨRegion polymorphism øApply what we did for type variables to region names (only it s more important and could be more onerous) void swap(int @`r1 x, int @`r2 y){ int tmp = *x; *x = *y; *y = tmp; } int@`r sumptr(region_t<`r> r,int x,int y){ return rnew(r) (x+y); }¡BkM EkCGþCgcgþcgcgþ cgþ cCC g ÿþ c g þ c g ÿþ c g þ c g þ c g þ c ª,Óóà¨Type definitions¨Kstruct ILst<`r1,`r2> { int@`r1 hd; struct ILst<`r1,`r2> *`r2 tl; }; ¡ L CgÿþC g ÿþCgÿþCgÿþ C $g$ÿþ(C(,g,ÿþ 0C000óá ¨Region subtyping ÒIf p points to an int in a region with name `r1, is it ever sound to give p type int*`r2? If so, let int*`r1 < int*`r2 Region subtyping is the outlives relationship {region r1; & {region r2; & } & } LIFO makes subtyping common ¡$[M!gÿþ g ÿþ CgÿþoÿþçÿGCgÿþnÿþçÿoÿþçÿ B F B $ C B C ª>ª óâ"¨Regions evaluationª ÆLIFO regions good for some idioms awkward in C Regions generalize stack variables and the heap Defaults and inference make it surprisingly palatable Worst part: defining region-allocated data structures Cyclone actually has much more [ISMM 04] Non-LIFO regions Unique pointers Explicitly reference-counted pointers A unified system , not n sublangages ¡/xf6)p/f6 a ªWóã#¨The plan from here ,Experience with Cyclone Not-NULL pointers Type-variable examples generics region-based memory management Brief view of everything else Related work ¡pA(-A( óä$¨Other safety holes JArrays (what or where is the size) Options: dynamic bound, in a field/variable, compile-time bound, special string support Threads (avoiding races) vaporware type system to enforce lock-based mutual exclusion Casts Allow only up casts and casts to numbers Unions Checked tags or bits-only fields Uninitialized data Flow analysis (safer and easier than default initializers) Varargs (safe via changed calling convention)¡î#X=+!;.#X=+ ! ;.ª> A'óå%¨And modern conveniences æ30 years after C, some things are worth adding& Tagged unions and pattern matching on them Intraprocedural type inference Tuples (like anonymous structs) Exceptions Struct and array initializers Namespaces new for allocation + initialization ¡Z0xÃ0 "ª>{ Hóê&¨Plenty of work remains¨ÓCommon limitations: Aliasing Arithmetic Unportable assumptions (But interoperating with C is much simpler than in a HLL) Big challenge for next generation: guarantees beyond fail-safe (i.e., graceful abort)¡X,:Y^rª( ¢óϨRelated work: making C safer ÊCompile to make dynamic checks possible Safe-C [Austin et al.], RTC [Yong/Horwitz], ... Purify, Stackguard, Electric Fence, & CCured [Necula et al.] performance via whole-program analysis less user burden less memory management, single-threaded Control-C [Adve et al.] weaker guaranty, less burden SFI [Wahbe, Small, ...]: sandboxing via binary rewriting ¡ð(ZmZ`ZpZZ(1` # ª>@aóí*¨Related Work: Checking C code `Model-checking C code (SLAM, BLAST, & ) Leverages scalability of MC Key is automatic building and refining of model Assumes (weak) memory safety Lint-like tools (Splint, Metal, PreFIX, & ) Good at reducing false positives Cannot ensure absence of bugs Metal particularly good for user-defined checks Cqual (user-defined qualifiers, lots of inference) Better for unchangeable code or user-defined checks (i.e., they re complementary)¡Î'ZiZ+ZoZ4ZSZ'L+!H3 SªPs6t,Tóð,¨Related work: higher and lower ¸Adapted/extended ideas: polymorphism [ML, Haskell, & ] regions [Tofte/Talpin, Walker et al., & ] safety via dataflow [Java, & ] existential types [Mitchell/Plotkin, & ] controlling data representation [Ada, Modula-3, & ] Safe lower-level languages [TAL, PCC, & ] engineered for machine-generated code Vault: stronger properties via restricted aliasing ¡Á)'4À)&4óѨSummary òCyclone: a safe language at the C-level of abstraction Synergistic combination of types, flow analysis, and run-time checks A real compiler and prototype applications Properties like not NULL , has longer lifetime , has array length & now in the language and checked Easy interoperability with C allow smooth and incremental move toward memory safety in theory at least¡zg7 E + g Uóî)¨ Availability Like any language, you have to kick the tires : www.research.att.com/projects/cyclone Also see: Jan. 2005 C/C++ User s Journal USENIX 2002 Conversely, I want to know NASA s C-level code needs Maybe ideas from Cyclone will help Maybe not Either way would be fascinating ¡¢1' +5-!1%Ìfþ +ª1Ìóæ¨ r[Presentation ends here some auxiliary slides follow]¡::óç¨Example in Cyclone¨void f(int@{`j} p, tag_t<`i> i, int v ; `i < `j){ p[i] = v; } Note: regions and locks use implicit defaults (live and accessible)¡ÌIEþÿ3þ ÿ3þ ÿ3þFª,"Róô0¨Some other problems \One safety violation typically renders all program properties potentially irrelevant So prohibit: incorrect casts, array-bounds violations, misused unions, uninitialized pointers, dangling pointers, null-pointer dereferences, dangling longjmp, vararg mismatch, not returning pointers, data races, & ¡,dZËZdË/ð¨ó^óÅ%óÐ&óè'óé(óï)Pÿÿÿêî<ï ùPØ ðÐð ð$ð( ð ð ðr ð Sð´\¿ÿ ðÀ°Ððà ð ðr ð Sðp]¿ÿ ðð°Ððà ð ðH ð ð0Þ½h¿ÿ ?ð ÿÿÿÌ33ÌÌÌÿ²²²80º___PPT10ë.óñÄ`Ö¦Árð.íhºõ)íÌ.¬¼ôCèÊ
é(à8Ø òú/È 0ÒÕ0·DTimes New Roman©Ñ´ÕÕì 0´ÕWo 0·DArialNew Roman©Ñ´ÕÕì 0´ÕWo 0" ·DCourier Newman©Ñ´ÕÕì 0´ÕWo 010·DWingdingswman©Ñ´ÕÕì 0´ÕWo 0¤ `ÿÿÿÿ¥ .© @£nÿý?" dd@ÿÿïÿÿÿÿÿÿ @@`` ðüð@u./ /7ZM)*@180c //2 $3)-0:13 !#"#$%&'()*+, 2 ./ð0A¿ÀÅAÿpñÿ3ÌfÌfÿÿÿfÿ@ñ÷ð8óóÐÑððnÊ;ÇÊ;úgþý4OdOdì 0¨Õ¤þÿÿ¬ÿÿÿpûppû@<ý4!d!d® 0dÙªÑ<ý4dddd® 0dÙªÑ<ý4BdBd® 0dÙªÑÿ N0º___PPT10 ÀÀº___PPT9ð®è¯¬`ÿÿÿÿÿÿ¯¬Xÿÿ?ÙdÚ-º11 January 2005 º*Dan Grossman: CycloneOÙ Ú=ðÛuó¨4Cyclone: A Memory-Safe C-Level Programming Language ¡"53 Ìfþ¨¬Dan Grossman University of Washington Joint work with: Trevor Jim AT&T Research Greg Morrisett Harvard University Michael Hicks University of Maryland¡:'(&Ìfþó¨A safe C-level language¨ Cyclone is a programming language and compiler aimed at safe systems programming C is not memory safe: void f(int* p, int i, int v) { p[i] = v; } Address p+i might hold important data or code Memory safety is crucial for reasoning about programs ¡S9h:ÿ3þÿ3þ þþþþ $ 6óà "Caller s problem?ª¨Ã void g(void**, void*); int y = 0; int *z = &y; g(&z,0xBAD); *z = 123; Might be safe, but not if g does *x=y Type of g enough for code generation Type of g not enough for safety checking¡$N v þþ þ!%ª> s& óë'¨Safe low-level systems¨8For a safety guarantee today, use YFHLL Your Favorite High Level Language YFHLL provides safety in part via: hidden data fields and run-time checks automatic memory management Data representation and resource management are essential aspects of low-level systems There are strong reasons for C-like languages¡(##D$Y.(ÌfþÌfþÌfþÌfþÌfþ#ÿ3þ! ÿ3þ0 ÿ3þ-óì(¨Some insufficient approaches ®Compile C with extra information type fields, size fields, live-pointer table, & treats C as a higher-level language Use static analysis very difficult less modular Ban unsafe features there are many you need them¡!U!T óǨCyclone in brief *A safe, convenient, and modern language at the C level of abstraction Safe: memory safety, abstract types, no core dumps C-level: user-controlled data representation and resource management, easy interoperability, manifest cost Convenient: may need more type annotations, but work hard to avoid it Modern: add features to capture common idioms New code for legacy or inherently low-level systems ¡ôGZZ6ZZFÿþÿþ. e ; '6óȨThe plan from here êExperience with Cyclone Benchmarks, ports
¡¢£¤¥¦§¨©ª«¬®¯°±²³´µ¶·¸¹º»¼½¾¿ÀÁÂÃÄÅÆÇÈÉÊËÌÍÎÏÐÑÒÓÔÕÖרÙÚÛÜÝÞßàáâãäåæçèéêëìíîïðñòóôõþÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿÿ, systems, compiler, & All on Earth so far Jð Not-NULL pointers Type-variable examples generics region-based memory management Brief view of everything else Related work Really just a taste of Cyclone¡ÂZ>Z)Z(Z-Z"Z< (-"óɨStatus ® Cyclone really exists (except memory-safe threads) >150K lines of Cyclone code, including the compiler gcc back-end (Linux, Cygwin, OSX, Mindstorm, & ) User s manual, mailing lists, & Still a research vehicle ¡À4¢34 0 ª ?óʨ Evaluation¨æ Is Cyclone like C? port code, measure source differences interface with C code (extend systems) What is the performance cost? port code, measure slowdown Is Cyclone good for low-level systems? write systems, ensure scalability ¡Ê" N" '" "N '"óË ¨Code differences¨Porting not automatic, but quite similar Many changes identify arrays and lengths Some changes incidental (absent prototypes, new keywords)¡óÌ ¨Run-time performance¨ÐRHLinux 7.1 (2.4.9), 1.0GHz PIII, 512MRAM, gcc2.96 -O3, glibc 2.2.4 Comparable to other safe languages to start C level provides important optimization opportunities Understanding the applications could help¡LED,6*óͨLarger program: the compiler¨Ö Scalable compiler + libraries (80K lines) build in < 30secs Generic libraries (e.g., lists, hashtables) clients have no syntactic/performance cost Static safety helps exploit the C-level I use &x more than in C ¡¼ 4,,( 3 ,+ ( óÎ ¨Other projects¨oOpen Kernel Environment [Bos/Samwel, OPENARCH 02] MediaNet [Hicks et al, OPENARCH 03]: RBClick [Patel/Lepreau, OPENARCH 03] STP [Patel et al., SOSP 03] FPGA synthesis [Teifel/Manohar, ISACS 04] Maryland undergrad O/S course (geekOS) [2004] Windows device driver (6K lines) Only 100 lines left in C But unrecoverable failures & other kernel corruptions remain ¡PWPP ' !Wªt =,óÒ¨The plan from here ,Experience with Cyclone Not-NULL pointers Type-variable examples generics region-based memory management Brief view of everything else Related work ¡zA(-(-óÓ¨Not-null pointersª óÔ¨Example êFILE* fopen(const char@, const char@); int fgetc(FILE@); int fclose(FILE@); void g() { FILE* f = fopen( foo , r ); int c; while((c = fgetc(f)) != EOF) {& } fclose(f); } Gives warning and inserts one null-check Encourages a hoisted check¡Ü±ZEZþ þ þþ þQDª aóÕ¨A classic moral¨LFILE* fopen(const char@, const char@); int fgetc(FILE@); int fclose(FILE@); ¡Mþ þ þ ª,1 óÖ!¨Key Design Principles in Action¨KTypes to express invariants Preconditions for arguments Properties of values in memory Flow analysis where helpful Lets users control explicit checks Soundness + aliasing limits usefulness Users control data representation Pointers are addresses unless user allows otherwise Often can interoperate with C more safely just via types¡°Z;ZZJZ"Z4Z9Z;#'"49ª$Rñóò. (It s always aliasing¨¿But can avoid checks when compiler knows all aliases. Can know by: Types: precondition checked at call site Flow: new objects start unaliased Else user should use a temporary (the safe thing)¡ C}Àª 3óó/ (It s always aliasing¨¿But can avoid checks when compiler knows all aliases. Can know by: Types: precondition checked at call site Flow: new objects start unaliased Else user should use a temporary (the safe thing)¡ C}Àª 3óñ-¨The plan from here ,Experience with Cyclone Not-NULL pointers Type-variable examples generics region-based memory management Brief view of everything else Related work ¡pA(-*(-óØ ( Change void* to `a ¡:¨struct Lst { void* hd; struct Lst* tl; }; struct Lst* map( void* f(void*), struct Lst*); struct Lst* append( struct Lst*, struct Lst*);¡\ ;þ1þ!óÙ¨Not much new here¨Closer to C than C++, Java generics, ML, etc. Unlike functional languages, data representation may restrict `a to pointers, int why not structs? why not float? why int? Unlike templates, no code duplication or leaking implementations Unlike objects, no need to tag data¡Ú/S)f/"N"c""c"c" " f"ª¦ióÚ¨Existential types Programs need a way for call-back types: struct T { void (*f)(void*, int); void* env; }; We use an existential type (simplified): struct T { <`a> void (@f)(`a, int); `a env; }; more C-level than baked-in closures/objects ¡+ZA0ZZ*ZA0Z,8ZZ+>" ÿþgÿþGÿþgÿ3þ gÿ3þ, "óÛ¨Regions a.k.a. zones, arenas, & Every object is in exactly one region Allocation via a region handle Deallocate an entire region simultaneously (cannot free an object) Old idea with recent support in languages (e.g., RC, RTSJ) and implementations (e.g., ML Kit)¡²|Z*ZZ_Z&7 _ª>`F. %óܨCyclone regions [PLDI 02]¡ heap region: one, lives forever, conservatively GC d stack regions: correspond to local-declaration blocks: {int x; int y; s} growable regions: scoped lifetime, but growable: {region r; s} allocation routines take a region handle handles are first-class caller decides where, callee decides how much no handles for stack regions¡m4B K (*þþ#þ".ÿ3þªb,1\óÝ (That s the easy part¨cThe implementation is really simple because the type system statically prevents dangling pointers ¡hd ÿþóÞ¨The big restriction ÎAnnotate all pointer types with a region name (a type variable of region kind) int@`r means pointer into the region created by the construct that introduces `r heap introduces `H L:& introduces `L {region r; s} introduces `r r has type region_t<`r> compile-time check: only live regions are accessed by default, function arguments point to live regions ¡PS$B² 35"" GgI"c"bc"c "cgþc "c" " c " c c 3b5bcªP¡''jóߨRegion polymorphism øApply what we did for type variables to region names (only it s more important and could be more onerous) void swap(int @`r1 x, int @`r2 y){ int tmp = *x; *x = *y; *y = tmp; } int@`r sumptr(region_t<`r> r,int x,int y){ return rnew(r) (x+y); }¡BkM EkCGþCgcgþcgcgþ cgþ cCC g ÿþ c g þ c g ÿþ c g þ c g þ c g þ c ª,Óóà¨Type definitions¨Kstruct ILst<`r1,`r2> { int@`r1 hd; struct ILst<`r1,`r2> *`r2 tl; }; ¡ L CgÿþC g ÿþCgÿþCgÿþ C $g$ÿþ(C(,g,ÿþ 0C000óá ¨Region subtyping ÒIf p points to an int in a region with name `r1, is it ever sound to give p type int*`r2? If so, let int*`r1 < int*`r2 Region subtyping is the outlives relationship {region r1; & {region r2; & } & } LIFO makes subtyping common ¡$[M!gÿþ g ÿþ CgÿþoÿþçÿGCgÿþnÿþçÿoÿþçÿ B F B $ C B C ª>ª óâ"¨Regions evaluationª ÆLIFO regions good for some idioms awkward in C Regions generalize stack variables and the heap Defaults and inference make it surprisingly palatable Worst part: defining region-allocated data structures Cyclone actually has much more [ISMM 04] Non-LIFO regions Unique pointers Explicitly reference-counted pointers A unified system , not n sublangages ¡/xf6)p/f6 a ªWóã#¨The plan from here ,Experience with Cyclone Not-NULL pointers Type-variable examples generics region-based memory management Brief view of everything else Related work ¡pA(-A( óä$¨Other safety holes JArrays (what or where is the size) Options: dynamic bound, in a field/variable, compile-time bound, special string support Threads (avoiding races) vaporware type system to enforce lock-based mutual exclusion Casts Allow only up casts and casts to numbers Unions Checked tags or bits-only fields Uninitialized data Flow analysis (safer and easier than default initializers) Varargs (safe via changed calling convention)¡î#X=+!;.#X=+ ! ;.ª> A'óå%¨And modern conveniences æ30 years after C, some things are worth adding& Tagged unions and pattern matching on them Intraprocedural type inference Tuples (like anonymous structs) Exceptions Struct and array initializers Namespaces new for allocation + initialization ¡Z0xÃ0 "ª>{ Hóê&¨Plenty of work remains¨ÓCommon limitations: Aliasing Arithmetic Unportable assumptions (But interoperating with C is much simpler than in a HLL) Big challenge for next generation: guarantees beyond fail-safe (i.e., graceful abort)¡X,:Y^rª( ¢óϨRelated work: making C safer ÊCompile to make dynamic checks possible Safe-C [Austin et al.], RTC [Yong/Horwitz], ... Purify, Stackguard, Electric Fence, & CCured [Necula et al.] performance via whole-program analysis less user burden less memory management, single-threaded Control-C [Adve et al.] weaker guaranty, less burden SFI [Wahbe, Small, ...]: sandboxing via binary rewriting ¡ð(ZmZ`ZpZZ(1` # ª>@aóí*¨Related Work: Checking C code `Model-checking C code (SLAM, BLAST, & ) Leverages scalability of MC Key is automatic building and refining of model Assumes (weak) memory safety Lint-like tools (Splint, Metal, PreFIX, & ) Good at reducing false positives Cannot ensure absence of bugs Metal particularly good for user-defined checks Cqual (user-defined qualifiers, lots of inference) Better for unchangeable code or user-defined checks (i.e., they re complementary)¡Î'ZiZ+ZoZ4ZSZ'L+!H3 SªPs6t,Tóð,¨Related work: higher and lower ¸Adapted/extended ideas: polymorphism [ML, Haskell, & ] regions [Tofte/Talpin, Walker et al., & ] safety via dataflow [Java, & ] existential types [Mitchell/Plotkin, & ] controlling data representation [Ada, Modula-3, & ] Safe lower-level languages [TAL, PCC, & ] engineered for machine-generated code Vault: stronger properties via restricted aliasing ¡Á)'4À)&4óѨSummary òCyclone: a safe language at the C-level of abstraction Synergistic combination of types, flow analysis, and run-time checks A real compiler and prototype applications Properties like not NULL , has longer lifetime , has array length & now in the language and checked Easy interoperability with C allow smooth and incremental move toward memory safety in theory at least¡zg7 E + g Uóî)¨ Availability Like any language, you have to kick the tires : www.research.att.com/projects/cyclone Also see: Jan. 2005 C/C++ User s Journal USENIX 2002 Conversely, I want to know NASA s C-level code needs Maybe ideas from Cyclone will help Maybe not Either way would be fascinating ¡¢1' +5-!1%Ìfþ +ª1Ì/ð¨ó^óÅ%óÐ&óè'óé(óï)Pÿÿÿêrè¼õíļºBôCèÖ
é(à8Ø òú/È 0ÒÕ0·DTimes New RomanäÓy´ÕÕì 0´ÕWo 0·DArialNew RomanäÓy´ÕÕì 0´ÕWo 0" ·DCourier NewmanäÓy´ÕÕì 0´ÕWo 010·DWingdingswmanäÓy´ÕÕì 0´ÕWo 0¤ `ÿÿÿÿ¥ .© @£nÿý?" dd@ÿÿïÿÿÿÿÿÿ @@`` ðüð@u-/ /7ZM) @-80c //2 + $3 ):13# 2ð0A¿ÀÅAÿpñÿ3ÌfÌfÿÿÿfÿ@ñ÷ð8óóÐÝððnÊ;ÇÊ;úgþý4OdOdì 0¨Õ¤þÿÿ¬ÿÿÿpûppû@<ý4!d!d® 0dÙÐÔy<ý4dddd® 0dÙÐÔy<ý4BdBd® 0dÙÐÔyÿ Z0º___PPT10 ÀÀº___PPT9ü®ô¯¬lÿÿÿÿÿÿ¯¬Xÿÿ?ÙdÚ-º11 January 2005 º*Dan Grossman: CycloneOÙ Ú=ðÛuó¨4Cyclone: A Memory-Safe C-Level Programming Language ¡"53 Ìfþ¨¬Dan Grossman University of Washington Joint work with: Trevor Jim AT&T Research Greg Morrisett Harvard University Michael Hicks University of Maryland¡:'(&Ìfþó¨A safe C-level language¨ Cyclone is a programming language and compiler aimed at safe systems programming C is not memory safe: void f(int* p, int i, int v) { p[i] = v; } Address p+i might hold important data or code Memory safety is crucial for reasoning about programs ¡S9h:ÿ3þÿ3þ þþþþ $ 6óà "Caller s problem?ª¨Ã void g(void**, void*); int y = 0; int *z = &y; g(&z,0xBAD); *z = 123; Might be safe, but not if g does *x=y Type of g enough for code generation Type of g not enough for safety checking¡$N v þþ þ!%ª> s& óë'¨Safe low-level systems¨8For a safety guarantee today, use YFHLL Your Favorite High Level Language YFHLL provides safety in part via: hidden data fields and run-time checks automatic memory management Data representation and resource management are essential aspects of low-level systems There are strong reasons for C-like languages¡(##D$Y.(ÌfþÌfþÌfþÌfþÌfþ#ÿ3þ! ÿ3þ0 ÿ3þ-óì(¨Some insufficient approaches ®Compile C with extra information type fields, size fields, live-pointer table, & treats C as a higher-level language Use static analysis very difficult less modular Ban unsafe features there are many you need them¡!U!T óǨCyclone in brief *A safe, convenient, and modern language at the C level of abstraction Safe: memory safety, abstract types, no core dumps C-level: user-controlled data representation and resource management, easy interoperability, manifest cost Convenient: may need more type annotations, but work hard to avoid it Modern: add features to capture common idioms New code for legacy or inherently low-level systems ¡ôGZZ6ZZFÿþÿþ. e ; '6óȨThe plan from here êExperience with Cyclone Benchmarks, ports, systems, compiler, & All on Earth so far Jð Not-NULL pointers Type-variable examples generics region-based memory management Brief view of everything else Related work Really just a taste of Cyclone¡ÂZ>Z)Z(Z-Z"Z< (-"óɨStatus ® Cyclone really exists (except memory-safe threads) >150K lines of Cyclone code, including the compiler gcc back-end (Linux, Cygwin, OSX, Mindstorm, & ) User s manual, mailing lists, & Still a research vehicle ¡À4¢34 0 ª ?óʨ Evaluation¨æ Is Cyclone like C? port code, measure source differences interface with C code (extend systems) What is the performance cost? port code, measure slowdown Is Cyclone good for low-level systems? write systems, ensure scalability ¡Ê" N" '" "N '"óË ¨Code differences¨Porting not automatic, but quite similar Many changes identify arrays and lengths Some changes incidental (absent prototypes, new keywords)¡óÌ ¨Run-time performance¨ÐRHLinux 7.1 (2.4.9), 1.0GHz PIII, 512MRAM, gcc2.96 -O3, glibc 2.2.4 Comparable to other safe languages to start C level provides important optimization opportunities Understanding the applications could help¡LED,6*óͨLarger program: the compiler¨Ö Scalable compiler + libraries (80K lines) build in < 30secs Generic libraries (e.g., lists, hashtables) clients have no syntactic/performance cost Static safety helps exploit the C-level I use &x more than in C ¡¼ 4,,( 3 ,+ ( óÎ ¨Other projects¨oOpen Kernel Environment [Bos/Samwel, OPENARCH 02] MediaNet [Hicks et al, OPENARCH 03]: RBClick [Patel/Lepreau, OPENARCH 03] STP [Patel et al., SOSP 03] FPGA synthesis [Teifel/Manohar, ISACS 04] Maryland undergrad O/S course (geekOS) [2004] Windows device driver (6K lines) Only 100 lines left in C But unrecoverable failures & other kernel corruptions remain ¡PWPP ' !Wªt =,óÒ¨The plan from here ,Experience with Cyclone Not-NULL pointers Type-variable examples generics region-based memory management Brief view of everything else Related work ¡zA(-(-óÓ¨Not-null pointersª óÔ¨Example êFILE* fopen(const char@, const char@); int fgetc(FILE@); int fclose(FILE@); void g() { FILE* f = fopen( foo , r ); int c; while((c = fgetc(f)) != EOF) {& } fclose(f); } Gives warning and inserts one null-check Encourages a hoisted check¡Ü±ZEZþ þ þþ þQDª aóÕ¨A classic moral¨LFILE* fopen(const char@, const char@); int fgetc(FILE@); int fclose(FILE@); ¡Mþ þ þ ª,1 óÖ!¨Key Design Principles in Action¨KTypes to express invariants Preconditions for arguments Properties of values in memory Flow analysis where helpful Lets users control explicit checks Soundness + aliasing limits usefulness Users control data representation Pointers are addresses unless user allows otherwise Often can interoperate with C more safely just via types¡°Z;ZZJZ"Z4Z9Z;#'"49ª$Rñóò. (It s always aliasing¨¿But can avoid checks when compiler knows all aliases. Can know by: Types: precondition checked at call site Flow: new objects start unaliased Else user should use a temporary (the safe thing)¡ C}Àª 3óó/ (It s always aliasing¨¿But can avoid checks when compiler knows all aliases. Can know by: Types: precondition checked at call site Flow: new objects start unaliased Else user should use a temporary (the safe thing)¡ C}Àª 3óñ-¨The plan from here ,Experience with Cyclone Not-NULL pointers Type-variable examples generics region-based memory management Brief view of everything else Related work ¡pA(-*(-óØ ( Change void* to `a ¡:¨struct Lst { void* hd; struct Lst* tl; }; struct Lst* map( void* f(void*), struct Lst*); struct Lst* append( struct Lst*, struct Lst*);¡\ ;þ1þ!óÙ¨Not much new here¨Closer to C than C++, Java generics, ML, etc. Unlike functional languages, data representation may restrict `a to pointers, int why not structs? why not float? why int? Unlike templates, no code duplication or leaking implementations Unlike objects, no need to tag data¡Ú/S)f/"N"c""c"c" " f"ª¦ióÚ¨Existential types Programs need a way for call-back types: struct T { void (*f)(void*, int); void* env; }; We use an existential type (simplified): struct T { <`a> void (@f)(`a, int); `a env; }; more C-level than baked-in closures/objects ¡+ZA0ZZ*ZA0Z,8ZZ+>" ÿþgÿþGÿþgÿ3þ gÿ3þ, "óÛ¨Regions a.k.a. zones, arenas, & Every object is in exactly one region Allocation via a region handle Deallocate an entire region simultaneously (cannot free an object) Old idea with recent support in languages (e.g., RC, RTSJ) and implementations (e.g., ML Kit)¡²|Z*ZZ_Z&7 _ª>`F. %óܨCyclone regions [PLDI 02]¡ heap region: one, lives forever, conservatively GC d stack regions: correspond to local-declaration blocks: {int x; int y; s} growable regions: scoped lifetime, but growable: {region r; s} allocation routines take a region handle handles are first-class caller decides where, callee decides how much no handles for stack regions¡m4B K (*þþ#þ".ÿ3þªb,1\óÝ (That s the easy part¨cThe implementation is really simple because the type system statically prevents dangling pointers ¡hd ÿþóÞ¨The big restriction ÎAnnotate all pointer types with a region name (a type variable of region kind) int@`r means pointer into the region created by the construct that introduces `r heap introduces `H L:& introduces `L {region r; s} introduces `r r has type region_t<`r> compile-time check: only live regions are accessed by default, function arguments point to live regions ¡PS$B² 35"" GgI"c"bc"c "cgþc "c" " c " c c 3b5bcªP¡''jóߨRegion polymorphism øApply what we did for type variables to region names (only it s more important and could be more onerous) void swap(int @`r1 x, int @`r2 y){ int tmp = *x; *x = *y; *y = tmp; } int@`r sumptr(region_t<`r> r,int x,int y){ return rnew(r) (x+y); }¡BkM EkCGþCgcgþcgcgþ cgþ cCC g ÿþ c g þ c g ÿþ c g þ c g þ c g þ c ª,Óóà¨Type definitions¨Kstruct ILst<`r1,`r2> { int@`r1 hd; struct ILst<`r1,`r2> *`r2 tl; }; ¡ L CgÿþC g ÿþCgÿþCgÿþ C $g$ÿþ(C(,g,ÿþ 0C000óá ¨Region subtyping ÒIf p points to an int in a region with name `r1, is it ever sound to give p type int*`r2? If so, let int*`r1 < int*`r2 Region subtyping is the outlives relationship {region r1; & {region r2; & } & } LIFO makes subtyping common ¡$[M!gÿþ g ÿþ CgÿþoÿþçÿGCgÿþnÿþçÿoÿþçÿ B F B $ C B C ª>ª óâ"¨Regions evaluationª ÆLIFO regions good for some idioms awkward in C Regions generalize stack variables and the heap Defaults and inference make it surprisingly palatable Worst part: defining region-allocated data structures Cyclone actually has much more [ISMM 04] Non-LIFO regions Unique pointers Explicitly reference-counted pointers A unified system , not n sublangages ¡/xf6)p/f6 a ªWóã#¨The plan from here ,Experience with Cyclone Not-NULL pointers Type-variable examples generics region-based memory management Brief view of everything else Related work ¡pA(-A( óä$¨Other safety holes JArrays (what or where is the size) Options: dynamic bound, in a field/variable, compile-time bound, special string support Threads (avoiding races) vaporware type system to enforce lock-based mutual exclusion Casts Allow only up casts and casts to numbers Unions Checked tags or bits-only fields Uninitialized data Flow analysis (safer and easier than default initializers) Varargs (safe via changed calling convention)¡î#X=+!;.#X=+ ! ;.ª> A'óå%¨And modern conveniences æ30 years after C, some things are worth adding& Tagged unions and pattern matching on them Intraprocedural type inference Tuples (like anonymous structs) Exceptions Struct and array initializers Namespaces new for allocation + initialization ¡Z0xÃ0 "ª>{ Hóê&¨Plenty of work remains¨ÓCommon limitations: Aliasing Arithmetic Unportable assumptions (But interoperating with C is much simpler than in a HLL) Big challenge for next generation: guarantees beyond fail-safe (i.e., graceful abort)¡X,:Y^rª( ¢óϨRelated work: making C safer ÊCompile to make dynamic checks possible Safe-C [Austin et al.], RTC [Yong/Horwitz], ... Purify, Stackguard, Electric Fence, & CCured [Necula et al.] performance via whole-program analysis less user burden less memory management, single-threaded Control-C [Adve et al.] weaker guaranty, less burden SFI [Wahbe, Small, ...]: sandboxing via binary rewriting ¡ð(ZmZ`ZpZZ(1` # ª>@aóí*¨Related Work: Checking C code `Model-checking C code (SLAM, BLAST, & ) Leverages scalability of MC Key is automatic building and refining of model Assumes (weak) memory safety Lint-like tools (Splint, Metal, PreFIX, & ) Good at reducing false positives Cannot ensure absence of bugs Metal particularly good for user-defined checks Cqual (user-defined qualifiers, lots of inference) Better for unchangeable code or user-defined checks (i.e., they re complementary)¡Î'ZiZ+ZoZ4ZSZ'L+!H3 SªPs6t,Tóð,¨Related work: higher and lower ¸Adapted/extended ideas: polymorphism [ML, Haskell, & ] regions [Tofte/Talpin, Walker et al., & ] safety via dataflow [Java, & ] existential types [Mitchell/Plotkin, & ] controlling data representation [Ada, Modula-3, & ] Safe lower-level languages [TAL, PCC, & ] engineered for machine-generated code Vault: stronger properties via restricted aliasing ¡Á)'4À)&4óѨSummary òCyclone: a safe language at the C-level of abstraction Synergistic combination of types, flow analysis, and run-time checks A real compiler and prototype applications Properties like not NULL , has longer lifetime , has array length & now in the language and checked Easy interoperability with C allow smooth and incremental move toward memory safety in theory at least¡zg7 E + g Uóî)¨ Availability Like any language, you have to kick the tires : www.research.att.com/projects/cyclone Also see: Jan. 2005 C/C++ User s Journal USENIX 2002 Conversely, I want to know NASA s C-level code needs Maybe ideas from Cyclone will help Maybe not Either way would be fascinating ¡¢1' +5-!1%Ìfþ +ª1Ì/ð¨ó^óÅ%óÐ&óè'óé(óï)PÿÿÿêrîBõíÊBÌÈôC
RetroSearch is an open source project built by @garambo
| Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4