Compiling first-order functions to session-typed parallel code

Building correct and efficient message-passing parallel pro-grams still poses many challenges. The incorrect use ofmessage-passing constructs can introduce deadlocks, anda bad task decomposition will not achieve good speedups.Current approaches focus either on correctness or efficiency,but limited work has been done on ensuring both. In thispaper, we propose a new parallel programming framework,PAlg, which is a first-order language withparticipant anno-tationsthat ensuresdeadlock-freedom by construction.PAlgprograms are coupled with an abstraction of their communi-cation structure, aglobal typefrom the theory ofmultipartysession types(MPST). This global type serves as an outputfor the programmer to assess the efficiency of their achievedparallelisation.PAlgis implemented as an EDSL in Haskell,from which we can: 1. compile to low-level message-passingC code; 2. compile to sequential C code, or interpret as se-quential Haskell functions; and, 3. infer the communicationprotocol followed by the compiled message-passing program.We use the properties of the inferred global types to performbasic message reordering optimisations to the compiled Ccode. We prove theextensional equivalenceof our outputparallelisation, as well as theprotocol compliance. We eval-uate our approach on a number of benchmarks. We achievelinear speedups on a shared-memory 12-core machine, anda speedup of 16 on a 2-node, 24-core NUMA