Share
Spores: A Type-Based Foundation for Closures in the Age of Concurrency and Distribution
Functional programming (FP) is regularly touted as the way forward for bringing parallel, concurrent, and distributed programming to the mainstream. The popularity of the rationale behind this viewpoint has even led to a number of object-oriented (OO) programming languages outside the Smalltalk tradition adopt- ing functional features such as lambdas and thereby function closures. However, despite this established viewpoint of FP as an enabler, reliably distributing function closures over a network, or using them in concurrent environments nonetheless remains a challenge across FP and OO languages. This paper takes a step towards more principled distributed and concurrent programming by introducing a new closure-like abstraction and type system, called spores, that can guarantee closures to be serializable, thread-safe, or even have custom user-defined properties. Crucially, our system is based on the principle of encoding type information corresponding to captured variables in the type of a spore. We prove our type system sound, implement our approach for Scala, evaluate its practicality through a small empirical study, and show the power of these guarantees through a case analysis of real-world distributed and concurrent frameworks that this safe foundation for closures facilitates.
Heather Miller
Transcript
59 slides
-
SPORES ECOOP 2014, Uppsala, Sweden August 1st, 2014 Heather Miller
A Type-Based Foundation for Closures in the Age of Concurrency & Distribution , Philipp Haller, Martin Odersky -
TWO TRENDS DATA-CENTRIC APPLICATIONS FUNCTIONAL PROGRAMMING APPLY FUNCTIONS TO IMMUTABLE
DATA. CLOSURE-HEAVY. CALLBACKS/REACTIVE. -
WHY? The basic philosophy to transform immutable data by applying
first-class functions. The observation that this functional style simplifies reasoning about data in parallel, concurrent, and distributed code. 1 2 -
Spark MapReduce DISTRIBUTED Java 8’s monadic optionally-parallel streams Scala’s parallel
collections Haskell’s Par Monad PARALLEL/ CONCURRENT Intel’s Concurrent Collections DATA-PARALLEL FRAMEWORKS -
Well, CLOSURES ARE OFTEN A SOURCE OF HEADACHES YOU CAN’T
REALLY DISTRIBUTE THEM. -
Well, CLOSURES ARE OFTEN A SOURCE OF HEADACHES NOT JUST
IN SCALA OR JAVA. BUT CROSS-PARADIGM. YOU CAN’T REALLY DISTRIBUTE THEM. -
PROBLEMS 1. Accidental capture of non-serializable variables (like this) 2.
Language-specific compilation schemes that create implicit references to objects that are not serializable 3. transitive references that inadvertently hold on to excessively large object graphs creating memory leaks THELAUNDRY LIST W/CLOSURES -
PROBLEMS 4. Capturing references to mutable objects, leading to race
conditions in a concurrent setting. 5. Unknowingly accessing object members that are not constant such as methods, which in a distributed setting can have logically different meanings on different machines. THELAUNDRY LIST W/CLOSURES CONT’D -
SPARK motivating example: http://docs.scala-lang.org/sips/pending/spores.html Scala Improvement Proposal: class MyCoolRddApp {
val param = 3.14 val log = new Log(...) ... def work(rdd: RDD[Int]) { rdd.map(x => x + param) .reduce(...) } } -
SPARK motivating example: http://docs.scala-lang.org/sips/pending/spores.html Scala Improvement Proposal: class MyCoolRddApp {
val param = 3.14 val log = new Log(...) ... def work(rdd: RDD[Int]) { rdd.map(x => x + param) .reduce(...) } } PROBLEM: not serializable because it captures this of type MyCoolRddApp which is itself not serializable (x => x + param) -
AKKA/FUTURES def receive = { case Request(data) =>
future { val result = transform(data) sender ! Response(result) } } Akka actor spawns future to concurrently process incoming results AKKA ACTOR SPAWNS A FUTURE TO CONCURRENTLY PROCESS INCOMING REQS NOT A STABLE VALUE! IT’S A METHOD CALL! PROBLEM: motivating example: http://docs.scala-lang.org/sips/pending/spores.html Scala Improvement Proposal: -
AKKA/FUTURES def receive = { case Request(data) =>
future { val result = transform(data) sender ! Response(result) } } Akka actor spawns future to concurrently process incoming results AKKA ACTOR SPAWNS A FUTURE TO CONCURRENTLY PROCESS INCOMING REQS NOT A STABLE VALUE! IT’S A METHOD CALL! PROBLEM: motivating example: http://docs.scala-lang.org/sips/pending/spores.html Scala Improvement Proposal: -
Need a solution that… INTEGRATES WITH EXISTING PRACTICE: PRACTICAL FOR
INCLUSION/ USE IN FULL-FEATURED SCALA. PRACTICAL FOR INTEGRATION WITH SPARK, AKKA, ETC. -
Need a solution that… ENABLES LIBRARY AUTHORS TO CONFIDENTLY RELEASE
LIBRARIES THAT EXPOSE FUNCTIONS IN USER-FACING APIS without concerns of runtime exceptions or other dubious errors falling on users. -
WHAT ARE THEY? A closure-like abstraction GOAL: Well-behaved closures with
controlled environments that can avoid various hazards. http://docs.scala-lang.org/sips/pending/spores.html Scala Improvement Proposal: SPORES A type system …designed for use in distributed or concurrent environments. -
http://docs.scala-lang.org/sips/pending/spores.html Scala Improvement Proposal: SPORES THIS IS ACHIEVED BY: (a)
enforcing a specific syntactic shape which dictates how the environment of a spore is declared. (b) providing additional type checking to ensure that types being captured have certain properties. -
http://docs.scala-lang.org/sips/pending/spores.html Scala Improvement Proposal: SPORES THIS IS ACHIEVED BY: (a)
enforcing a specific syntactic shape which dictates how the environment of a spore is declared. (b) providing additional type checking to ensure that types being captured have certain properties. CRUCIALLY, spores encode extra type information corresponding to the captured environment in their type. -
Contributions spores abstraction & type system type-based constraints that can
be combined with existing type systems formalization and soundness proof implementation of spores for Scala small empirical study of practicality -
Contributions spores abstraction & type system type-based constraints that can
be combined with existing type systems formalization and soundness proof implementation of spores for Scala small empirical study of practicality details in the paper… (covered in this presentation) -
WHAT DO SPORES LOOK LIKE? Basic usage: val s =
spore { val h = helper (x: Int) => { val result = x + " " + h.toString println("The result is: " + result) } } THE BODY OF A SPORE CONSISTS OF 2 PARTS 2 a closure a sequence of local value (val) declarations only (the “spore header”), and 1 http://docs.scala-lang.org/sips/pending/spores.html Scala Improvement Proposal -
WHAT DO SPORES LOOK LIKE? Basic usage: val s =
spore { val h = helper (x: Int) => { val result = x + " " + h.toString println("The result is: " + result) } } THE BODY OF A SPORE CONSISTS OF 2 PARTS 2 a closure a sequence of local value (val) declarations only (the “spore header”), and 1 http://docs.scala-lang.org/sips/pending/spores.html Scala Improvement Proposal -
WHAT DO SPORES LOOK LIKE? Basic usage: val s =
spore { val h = helper (x: Int) => { val result = x + " " + h.toString println("The result is: " + result) } } THE BODY OF A SPORE CONSISTS OF 2 PARTS 2 a closure a sequence of local value (val) declarations only (the “spore header”), and 1 http://docs.scala-lang.org/sips/pending/spores.html Scala Improvement Proposal -
SPORE 1. All captured variables are declared in the
spore header, or using capture 2. The initializers of captured variables are executed once, upon creation of the spore 3. References to captured variables do not change during the spore’s execution vsCLOSURES ( ) A Guarantees... http://docs.scala-lang.org/sips/pending/spores.html Scala Improvement Proposal: -
SPORES&CLOSURES EVALUATION SEMANTICS: Remove the spore marker, and the code
behaves as before SPORES & CLOSURES ARE RELATED: You can write a full function literal and pass it to something that expects a spore. (Of course, only if the function literal satisfies the spore rules.) http://docs.scala-lang.org/sips/pending/spores.html Scala Improvement Proposal: -
HOW CAN YOU USE A SPORE? Ok. So. IN APIS
http://docs.scala-lang.org/sips/pending/spores.html Scala Improvement Proposal def sendOverWire(s: Spore[Int, Int]): Unit = ... // ... sendOverWire((x: Int) => x * x -‐ 2) If you want parameters to be spores, then you can write it this way -
WHAT DOES ALL OF THAT http://docs.scala-lang.org/sips/pending/spores.html Scala Improvement Proposal GET
YOU? SINCE... Captured expressions are evaluated upon spore creation. ! Spores are like function values with an immutable environment. Plus, environment is specified and checked, no accidental capturing. THAT MEANS... -
KEEP TRACK OF CAPTURED TYPES Idea: The spore macro can
synthesize precise types automatically for newly created spores: Spore[Int, ...] { type Excluded = No[Actor] type Captured = (Int, ActorRef) } w/ constraints CreatingSPORES ...at compile-time spore { val x: Int = list.size; val a: ActorRef = this.sender (y: Int) => ... } without[Actor] SYNTHESIZED TYPE: -
w/ constraints ComposingSPORES BASIC COMPOSITION OPERATORS (same as for regular
functions) andThen compose How do we synthesize the result type of s1 andThen s2? RESULT TYPE SYNTHESIZED BY andThen MACRO type member Captured: concatenation of the captured types of s1 and s2 type member Excluded: conjunction of excluded types, needs to check Captured type members to see if possible -
w/ constraints Example:Composing val s1: Spore[Int, String] {
type Excluded = No[Actor] type Captured = (Int, ActorRef) } = ... val s2: Spore[String, String] { type Excluded = No[RDD[Int]] type Captured = Actor } s1 andThen s2 // does not compile SPORES -
w/ constraints Example: SPORES Composing val s1: Spore[Int, String] {
type Excluded = No[Actor] type Captured = (Int, ActorRef) } = ... val s2: Spore[String, String] { type Excluded = No[RDD[Int]] } s1 andThen s2: Spore[Int, String] { type Excluded = No[Actor] with No[RDD[Int]] type Captured = (Int, ActorRef) } ! -
PROPERTIES Enter: IDEA: http://docs.scala-lang.org/sips/pending/spores.html Scala Improvement Proposal case class Person(name:
String, age: Int) ! val fun = spore { val p: Person = ... val luckyNum: Int = ... () => s"${p.name}'s lucky number is: $luckyNum" } allow expressing a type-based property that must be satisfied by all captured variables upon creation of a spore. EXAMPLE: ENSURE THE FOLLOWING SPORE IS SERIALIZABLE. -
PROPERTIES Enter: IDEA: http://docs.scala-lang.org/sips/pending/spores.html Scala Improvement Proposal case class Person(name:
String, age: Int) ! val fun = spore { val p: Person = ... val luckyNum: Int = ... () => s"${p.name}'s lucky number is: $luckyNum" } allow expressing a type-based property that must be satisfied by all captured variables upon creation of a spore. EXAMPLE: ENSURE THE FOLLOWING SPORE IS SERIALIZABLE. To serialize a spore, it's necessary that for all captured variables of type T, there is an implicit pickler of type Pickler[T] in scope. -
PROPERTIES Enter: IDEA: http://docs.scala-lang.org/sips/pending/spores.html Scala Improvement Proposal case class Person(name:
String, age: Int) ! val fun = spore { val p: Person = ... val luckyNum: Int = ... () => s"${p.name}'s lucky number is: $luckyNum" } allow expressing a type-based property that must be satisfied by all captured variables upon creation of a spore. EXAMPLE: ENSURE THE FOLLOWING SPORE IS SERIALIZABLE. To serialize a spore, it's necessary that for all captured variables of type T, there is an implicit pickler of type Pickler[T] in scope. Pickler[T] CAN BE A SUCH A PROPERTY -
PROPERTIES Enter: WHAT ARE THEY? http://docs.scala-lang.org/sips/pending/spores.html Scala Improvement Proposal Properties
are defined using a type Property[T] Use a property by importing it. When importing a property of type Property[Prop] all spores in scope are guaranteed to satisfy the property or not compile (= all captured types have property Prop) -
PROPERTIES Enter: WHAT ARE THEY? http://docs.scala-lang.org/sips/pending/spores.html Scala Improvement Proposal Properties
are defined using a type Property[T] Use a property by importing it. When importing a property of type Property[Prop] all spores in scope are guaranteed to satisfy the property or not compile (= all captured types have property Prop) so, in the case of pickling, just: import picklable and the framework ensures that a Pickler[T] exists for every captured type T. (has to have type Property[Pickler]) -
NOT LIMITED TO PICKLING CAN HAVE ARBITRARY PROPERTIES. http://docs.scala-lang.org/sips/pending/spores.html Scala
Improvement Proposal …plugs in nicely with other pluggable type systems. Integrate with a deep immutability checker like OIGJ (Zibin et al. 2010) EXAMPLE: DEEP IMMUTABILITY -
NOT LIMITED TO PICKLING IDEA: http://docs.scala-lang.org/sips/pending/spores.html Scala Improvement Proposal Automatically
generate type class instances for all types that satisfy a transitive predicate, using macros. implicit def isImmutable[T: TypeTag]: Immutable[T] which returns a type class instance for all types of the shape C[O, Immut] that's deeply immutable (analyzing the TypeTag). -
NOT LIMITED TO PICKLING IDEA: http://docs.scala-lang.org/sips/pending/spores.html Scala Improvement Proposal Automatically
generate type class instances for all types that satisfy a transitive predicate, using macros. implicit def isImmutable[T: TypeTag]: Immutable[T] which returns a type class instance for all types of the shape C[O, Immut] that's deeply immutable (analyzing the TypeTag). To enforce transitive immutability for a spore, it's then sufficient to define an implicit of type Property[Immutable]. -
FORMALIZATION CENTRAL IDEA: Spore types are refinements of function types.
| pn t SURSHUW\ LPSRUW | t t VSRUH FRPSRVLWLRQ v ::= (x : T) ⇒ t DEVWUDFWLRQ | {l = v} UHFRUG YDOXH | { x : T = v ; pn; (x : T) ⇒ t } VSRUH YDOXH T ::= T ⇒ T IXQFWLRQ W\SH | {l : T} UHFRUG W\SH | S S ::= T ⇒ T { C = T ; pn } VSRUH W\SH | T ⇒ T { C ; pn } DEVWUDFW VSRUH W\SH P ∈ pn → T SURSHUW\ PDS T ∈ P(T) W\SH IDPLO\ Γ ::= x : T W\SH HQYLURQPHQW ∆ ::= pn SURSHUW\ HQYLURQPHQW HU 3 +DOOHU DQG 0 2GHUVN\ ::= ... WHUPV | { x : T = t ; T; pn; (x : T) ⇒ t } VSRUH ::= ... YDOXHV | { x : T = v ; T; pn; (x : T) ⇒ t } VSRUH YDOXH ::= T ⇒ T { C = T ; E = T ; pn } VSRUH W\SH | T ⇒ T { C ; E = T ; pn } DEVWUDFW VSRUH W\SH )LJ &RUH ODQJXDJH V\QWD[ H[WHQVLRQV ϿϱЁζ T2 <: T1 R1 <: R2 n′ ⊆ pn M1 = M2 ∨ M2 = C ∀T′ ∈ U′. ∃T ∈ U. T′ <: They include more information than typical functions: properties, excluded, and captured -
FORMALIZATION This additional information is used when type- checking (assume
S1 and S2 are the types of two spores): properties: S1 <: S2 implies S1 must satisfy at least the properties of S2 excluded: S1 <: S2 implies S1 must exclude at least the types that S2 excludes captured: S1 <: S2 implies S2 either has abstract type Captured or S1 and S2 agree on the captured types (Intuition) -
FORMALIZATION This additional information is used when type- checking (assume
S1 and S2 are the types of two spores): properties: S1 <: S2 implies S1 must satisfy at least the properties of S2 excluded: S1 <: S2 implies S1 must exclude at least the types that S2 excludes captured: S1 <: S2 implies S2 either has abstract type Captured or S1 and S2 agree on the captured types (Intuition) -
FORMALIZATION Sound composition of constraints: avoid calculating constraints that are
not guaranteed to hold at runtime SPORE COMPOSITION PRESERVES TYPE CONSTRAINTS …In the paper: ! Soundness proof based on a small-step operational semantics and progress+preservation. ! Correspondence to the Scala implementation -
MINI EMPIRICAL STUDY #1 + 0LOOHU 3 +DOOHU DQG
0 2GHUVN\ MOOC Parallel Collections Spark ^ ^ ^ EH LQIHUUHG D VHTXHQFH RI W\SHV VSHFLI\LQJ W\SH ERXQGV LV REWDLQHG DV IROORZV %DVL FDOO\ WKH W\SH RI WKH LPSOLFLW YDOXH LV PDWFKHG DJDLQVW WKH SDWWHUQ ƃɨƄ ŜŜŜ ƃƄ ZKHUH WKH DUH W\SH YDULDEOHV )RU HDFK W\SH DQ LPSOLFLW YDOXH PHPEHU ś ƃƄ ʰ ƃƃƄƄ LV JHQHUDWHG DQG DGGHG WR WKH UHILQHPHQW W\SH :H DOVR SURYLGH DQ LPSOLFLW FRQYHUVLRQ IURP VWDQGDUG 6FDOD IXQFWLRQV WR VSRUHV 7KLV FRQYHUVLRQ LV LPSOHPHQWHG DV D PDFUR ZKRVH H[SDQVLRQ IDLOV LI WKH DUJXPHQW IXQF WLRQ LV QRW D OLWHUDO VLQFH LQ WKLV FDVH LW LV LPSRVVLEOH IRU WKH PDFUR WR FKHFN WKH VSRUH VKDSHFDSWXULQJ FRQVWUDLQWV (YDOXDWLRQ 3URJUDP /2& FORVXUHV FRQYHUWHG /2& FKDQJHG FDSWXUHG YDUV IXQVHWV IRUFRPS PDQGHOEURW EDUQHVKXW VSDUN SDJHUDQN VSDUN NPHDQV 7RWDO )LJ &RPSDULVRQ WR UHODWHG DSSURDFKHV ,Q WKLV VHFWLRQ ZH HYDOXDWH WKH SUDFWLFDOLW\ RI XVLQJ VSRUHV DV DQ DOWHUQDWLYH WR QRUPDO FORVXUHV LQ 6FDOD E\ PHDVXULQJ WKH QXPEHU RI FKDQJHV UHTXLUHG WR FRQYHUW H[LVWLQJ SUR JUDPV WKDW FUXFLDOO\ UHO\ RQ FORVXUHV WR XVH VSRUHV :H DQDO\]H D QXPEHU RI UHDO 6FDOD SURJUDPV WDNHQ IURP WKUHH FDWHJRULHV *HQHUDO FORVXUHKHDY\ FRGH WDNHQ IURP WKH H[HUFLVHV RI WKH SRSXODU 022& RQ )XQFWLRQDO 3URJUDPPLQJ 3ULQFLSOHV LQ 6FDOD WKH JRDO RI DQDO\]LQJ WKLV FRGH LV WR JHW )LJ (YDOXDWLQJ WKH SUDFWLFDOLW\ RI XVLQJ VSRUHV LQ SODFH RI QRUPDO FORVXUHV YDOXH LV PDWFKHG DJDLQVW WKH SDWWHUQ ƃɨƄ ŜŜŜ ƃƄ )RU HDFK W\SH DQ LPSOLFLW PHPEHU RI WKH IROORZLQJ VKDSH LV DGGHG WR WKH W\SH UHILQHPHQW ś ƃƄ ʰ ƃƃƄƄ 7KH LPSOLFLW FRQYHUVLRQ 6HFWLRQ IURP VWDQGDUG 6FDOD IXQFWLRQV WR VSRUHV LV LPSOH PHQWHG DV D PDFUR ZKRVH H[SDQVLRQ IDLOV LI WKH DUJXPHQW IXQFWLRQ LV QRW D OLWHUDO VLQFH How much effort is required to convert existing programs that crucially rely on closures to spores? For each closure, we had to change 1.4LOC on average, or only 45/1503 LOC -
6SRUHV $ 7\SH%DVHG )RXQGDWLRQ IRU &ORVXUHV LQ WKH $JH RI
&RQFXUUHQF\ 'LVWULEXWLRQ DYHUDJH /2& DYHUDJH RI FORVXUHV WKDW 3URMHFW SHU FORVXUH FDSWXUHG YDUV GRQ¶W FDSWXUH ŵ LOC Şŵ LOC ŵ LOC ŵŞ LOC ŵ Ş LOC ŵŞŞ LOC ŵ LOC 7RWDO LOC )LJ (YDOXDWLQJ WKH LPSDFW DQG RYHUKHDG RI VSRUHV RQ UHDO GLVWULEXWHG DSSOLFDWLRQV MINI EMPIRICAL STUDY #2 How widespread are patterns that can be statically enforced by spores? -
6SRUHV $ 7\SH%DVHG )RXQGDWLRQ IRU &ORVXUHV LQ WKH $JH RI
&RQFXUUHQF\ 'LVWULEXWLRQ DYHUDJH /2& DYHUDJH RI FORVXUHV WKDW 3URMHFW SHU FORVXUH FDSWXUHG YDUV GRQ¶W FDSWXUH ŵ LOC Şŵ LOC ŵ LOC ŵŞ LOC ŵ Ş LOC ŵŞŞ LOC ŵ LOC 7RWDO LOC )LJ (YDOXDWLQJ WKH LPSDFW DQG RYHUKHDG RI VSRUHV RQ UHDO GLVWULEXWHG DSSOLFDWLRQV MINI EMPIRICAL STUDY #2 How widespread are patterns that can be statically enforced by spores? 67.2% of all closures can be automatically converted. The remaining 32.8% capture only 1.39 variables on average. ! Thus, unchecked patterns are widespread in real applications, and require only little overhead to enable spore guarantees.