Read-OnlySpecificationsforBetterSynthesisofProgramswithPointers AndreeaCostea1,AmyZhu2,NadiaPolikarpova3,andIlyaSergey4,1 1SchoolofComputing,NationalUniversityofSingapore,Singapore2UniversityofBritishColumbia,Vancouver,Canada3UniversityofCalifornia,SanDiego,USA4Yale-NUSCollege,Singapore Abstract.Inprogramsynthesisthereisawell-knowntrade-offbetweenconciseandstrongspecifications:ifaspecificationistooverbose,itmightbehardertowritethantheprogram;ifitistooweak,thesynthesisedprogrammightnotmatchtheuser’sintent.Inthisworkweexploretheuseofannotationsforrestrictingmemoryesspermissionsinprogramsynthesis,andshowthattheycanmakespecificationsmuchstrongerwhileremainingsurprisinglyconcise.Specifically,weenhanceSyntheticSeparationLogic(SSL),aframeworkforsynthesisofheap-manipulatingprograms,withthelogicalmechanismofread-onlyborrows. WeobservethatthisminimalisticandconservativeSSLextensionbenefitsthesynthesisinseveralways,makingitmore(a)expressive(strongercorrectnessguaranteesareachievedwithamodestannotationoverhead),(b)effective(itproducesmoreconciseandeasier-to-readprograms),(c)efficient(fastersynthesis),and(d)robust(synthesisefficiencyislessaffectedbythechoiceofthesearchheuristic).Weexplaintheintuitionandprovideformaltreatmentforread-onlyborrows.Wesubstantiatetheclaims(a)–(d)bydescribingourquantitativeevaluationoftheborrowing-awaresynthesisimplementationonaseriesofstandardbenchmarkspecificationsforvariousheap-manipulatingprograms. 1Introduction Deductiveprogramsynthesisisaprominentapproachtothegenerationofcorrectby-constructionprogramsfromtheirdeclarativespecifications[14,23,29,33].Withthismethodology,onecanrepresentsearchingforaprogramsatisfyingtheuser-providedconstraintsasaproofsearchinacertainlogic.Followingthisidea,ithasbeenrecentlyobserved[34]thatthesynthesisofcorrect-by-constructionimperativeheap-manipulatingprograms(inalanguagesimilartoC)canbeimplementedasaproofsearchinaversionofSeparationLogic(SL)—aprogramlogicdesignedformodularverificationofprogramswithpointers[32,37]. SL-baseddeductiveprogramsynthesisbasedonSyntheticSeparationLogic(SSL)[34]requirestheprogrammertoprovideaHoare-stylespecificationforaprogramofinterest.Forinstance,giventhepredicatels(x,S),whichdenotesasymbolicheapcorrespondingtoalinkedliststartingatapointerx,endingwithnull,andcontainingelementsfromthesetS,onecanspecifythebehaviouroftheprocedureforcopyingalinkedlistasfollows: {r→x∗ls(x,S)}listcopy(r){r→y∗ls(x,S)∗ls(y,S)}
(1) WorkdoneduringaninternshipatNUSSchoolofComputinginSummer2019. ©TheAuthor(s)2020P.Mu¨ller(Ed.):ESOP2020,LNCS12075,pp.141–168,2020./10.1007/978-3-030-44914-8_
6 142A.Costeaetal. z ls(n}x|t,S′) { contentx vnxt v′nxt′… wnull addressr xx+
1 nxtnxt+
1 z }| { ls(x,S) Thepreconditionofspecification
(1),definingtheshapeoftheinitialheap,isillustratedbythefigureabove.Itrequirestheheaptocontainapointerr,whichistakenbytheprocedureasanargumentandwhosestoredvalue,x,istheheadpointerofthelisttobecopied.Thelistitselfisdescribedbythesymbolicheappredicateinstancels(x,S),whosefootprintisassumedtobedisjointfromtheentryr→x,followingthestandardsemanticsoftheseparatingconjunctionoperator(∗)[32].Thepostconditionassertsthatthefinalheap,inadditiontocontainingtheoriginallistls(x,S),willcontainanewliststartingfromywhosecontentsSarethesameasoftheoriginallist,andalsothatthepointerrwillnowpointtotheheadyofthelistcopy.Ourspecificationisplete:itallows,forexample,duplicatingorrearrangingelements.Onehopesthatsuchaprogramisunlikelytobesynthesised.Insynthesis,itmontoprovidepletespecs:pleteonescanbeashardaswritingtheprogramitself. 1.1CorrectProgramsthatDoStrangeThings Providedthedefinitionoftheheappredicatelsandthespecification
(1),theSuS- 1voidlistcopy(locr){2letx=*r; Liktool,animplementationoftheSSL-3basedsynthesis[34],willproducethepro-4gramdepictedinFig.1.Itiseasytocheck5 6 thatthisprogramsatisfiestheascribed7 spec
(1).Moreover,itcorrectlyduplicates8 if(x==0){}else{ letv=*x;letnxt=*(x+1);*r=nxt;listcopy(r); theoriginallist,faithfullypreservingits9 contentsandtheordering.However,an10astutereadermightnoticeacertainodd-11 12 ityinthewayittreatstheinitiallistpro-13videdforcopying.ordingtothepost-14 lety1=*r;lety=malloc
(2);*(x+1)=y1;*r=y;*(y+1)=nxt;*y=v; conditionof
(1),thevalueofthepointer15}} rstoredinalocalimmutablevariabley1 z ls(x,S)}| { online9istheheadofthecopyoftheoriginallist’stail.Quiteunexpectedly,they vy1 v′… … pointery1esthetailoftheoriginalr xx+
1 nxtnxt+
1 listonline11,whiletheoriginallist’stailpointernxt,onceassignedto*(y+1)online13,esthetailofthecopy!
Indeed,theexerciseintailswappingistotallypointless:notonlydoesitproducesless“natural”andreadablecode,butthe vnxt v′… … yy+
1 y1y1+
1 z }| { ls(y,S) Fig.1:Resultprogramforspec(1)andtheshapeofitsfinalheap. resultingprogram’slocalitypropertiesareunsatisfactory;forinstance,thispro- ConciseRead-OnlySpecificationsforBetterSynthesis143 gramcannotbepluggedintoaconcurrentsettingwheremultiplethreadsrelyonls(x,S)tobeunchanged. TheissuewiththeresultinFig.1iscausedbyspecification(1)beingtoopermissive:itdoesnotpreventthesynthesisedprogramfrommodifyingthestructureoftheinitiallist,whilecreatingitscopy.Luckily,themunityhasdevisedanumberofSLextensionsthatallowonetoimposesuchrestrictions,likedeclaringapartoftheprovidedsymbolicheapasread-only[5,8,9,11,15,20,21],i.e.,forbiddentomodifybythespecifiedcode. 1.2TowardsSimpleRead-OnlySpecificationsforSynthesis Themainchallengeofintroducingread-onlyannotationsmonlyalsoreferredtoaspermissions)5intoSeparationLogicliesinestablishingthedisciplineforperformingsoundountinginthepresenceofmixedread-onlyandmutatingheapessesbydiffponentsofaprogram. Asanexample,considerasimplesymbolicheapx→Mf∗r→Mhthatdeclares twomutable(i.e.,allowedtobewrittento)pointersxandr,thatpointtounspecifiedvaluesfandh,correspondingly.Withthissymbolicheap,isitsafetocallthefollowingfunctionthatmodifiesthecontentsofrbutnotofx?
x→ROf∗r→MhreadX(x,r)x→ROf∗r→Mf
(2) ThepreconditionofreadXrequiresaweakerformofesspermissionforx(read-only,RO),whiletheconsideredheapassertsastrongerwritepermission(M).ItshouldbepossibletosatisfyreadX’srequirementbyprovidingthenecessaryread-onlypermissionforx.Todoso,weneedtoagreeonadisciplineto“adapt”thecaller’swrite-permissionMtothecallee’sread-onlypermissionRO.Whileseeminglytrivial,ifimplementedna¨ıvely,ountingofROpermissionsinSLpromiseeithersoundnesspletenessofthelogicalreasoning. Anumberofproposalsforlogicallysoundinterplaybetweenwrite-andreadonlyesspermissionsinthepresenceoffunctioncallshasbeendescribedintheliterature[7–9,11,13,20,30].Someoftheseworksmanagetomaintainthesimplicityofhavingonlymutable/read-onlyannotationswhenconfinedtothesequentialsetting[9,11,13].Moregeneral(buthardertoimplement)approachesrelyonfractionalpermissions[8,25],anexpressivemechanismforpermissionounting,withprimaryapplicationsinconcurrentreasoning[7,28].Westartedthisprojectbyattemptingtoadaptsomeofthoselogics[9,11,13]asanextensionofSSLinordertoreapthebenefitsofread-onlyannotationsforthesynthesisofsequentialprogram.Themainobstacleweencounteredinvolveddefinitionsofinductiveheappredicateswithmixedpermissions.Forinstance,howcanonespecifyaprogramthatmodifiesthecontentsofalinkedlist,butnotitsstructure?
Eventhoughitseemedpossibletoenablethistreatmentofpredicatesviapermissionmultiplication[25],developingsupportforthismachineryofexistingSuSLikinfrastructurewasadauntingtask.Therefore,wehadtolookforatechnicallysimplersolution. 5Wewillbeusingthewords“annotation”and“permission”interchangeably. 144A.Costeaetal. 1.3OurContributions TheoreticalContributions.OurmainconceptualinnovationistheideaofinstrumentingSSLwithsymbolicread-onlyborrowstoenablefasterandmorepredictableprogramsynthesis.Borrowsareusedtoannotatesymbolicheapsinspecifications,similarlytoabstractfractionalpermissionsfromthedeductiveverificationtools,suchasChaliceandVeriFast[20,21,27].Theyenablesimplebutprincipledlightweightthreadingofheapesspermissionsfromthecallerstocalleesandback,whileenforcingread-onlyesswheneveritisrequired.Forbasicintuitiononread-onlyborrows,considerthespecificationbelow: x→af∗y→bg∗r→MhreadXY(x,y,r)x→af∗y→bg∗r→M(f+g)
(3) Thepreconditionrequiresaheapwiththreepointers,x,y,andr,pointingtounspecifiedf,g,andh,correspondingly.Bothxandyaregoingtobetreatedasread-only,butnow,insteadofsimplyannotatingthemwithRO,weaddsymbolicborrowingannotationsaandb.Thesemanticsoftheseborrowingannotationsisthesameasthatofotherghostvariables(suchasf).Inparticular,thecalleemustbehavecorrectlyforanyvaluationofaandb,whichleavesitnochoicebuttotreatthecorrespondingheapfragmentsasread-only(hencepreventingtheheapfragmentsfrombeingwritten).Ontheotherhand,fromtheperspectiveofthecaller,theyserveasformalparametersthataresubstitutedwithactualsofcaller’schoosing:forinstance,wheninvokedwithacaller’ssymbolicheapx→M1∗y→c2∗r→M0(wherecdenotesaread-onlyborrowofthecaller), readXYisguaranteedto“restore”thesameesspermissionsinthepostcondition,asperthesubstitution[M/a,c/b].Theexampleabovedemonstratesthatread-onlyborrowsarestraightforwardposewhenreasoningaboutcodewithfunctioncalls.Theyalsomakeitpossibletodefineborrow-polymorphicinductiveheappredicates,e.g.,enhancinglsfromspec(1)soitcanbeusedinspecificationswithmixedesspermissionsonponents.6Finally,readonlyborrowsmakeitalmosttrivialtoadapttheexistingSSL-basedsynthesistoworkwithread-onlyesspermissions;theyreduceplexpermissionountingtoeasy-to-implementpermissionsubstitution. PracticalContributions.OurfirstpracticalcontributionisROBoSuSLik—anenhancementoftheSuSLiksynthesistool[34]withsupportforread-onlyborrows,whichrequiredustomodifylessthan100linesoftheoriginalcode. Oursecondpracticalcontributionistheextensiveevaluationofsynthesiswithread-onlypermissions,onastandardbenchmarksuiteofspecificationsforheapmanipulatingprograms.parethebehaviour,performance,andtheesofthesynthesiswhenrunwiththestandard(“all-mutable”)specificationsandtheiranaloguesinstrumentedwithread-onlypermissionswhereverreasonable.Bydoingso,wesubstantiatethefollowingclaimsregardingthepracticalimpactofusingread-onlyborrowsinSSLspecifications: –First,weshowthatsynthesisofread-onlyspecificationsismoreefficient:itdoeslessbacktrackingwhilesearchingforaprogramthatsatisfiestheimposedconstraints,entailingbetterperformance. 6Wewillpresentborrow-polymorphicinductiveheappredicatesinSec.2.4. ConciseRead-OnlySpecificationsforBetterSynthesis145 –Second,wedemonstratethatborrowing-awaresynthesisismoreeffective:specificationswithread-onlyannotationsleadtomoreconciseandhumanreadableprograms,whichdonotperformredundantoperations. –Third,weobservethatread-onlyborrowsincreaseexpressivityofthesynthesis:inmostofthecasesenhancedspecificationsprovidestrongercorrectnessguaranteesfortheresults,atalmostnoadditionalannotationoverhead. –Finally,weshowthatread-onlyborrowsmakethesynthesismorerobust:itsresultsandperformancearelesslikelytobeaffectedbytheunificationorderortheorderoftheattemptedruleapplicationsduringthesearch. PaperOutline.WestartbyshowcasingtheintricaciesandthevirtuesofSSLbasedsynthesiswithread-onlyspecificationsinSec.2.Weprovidetheformalountofread-onlyborrowsandpresentthemodifiedSSLrules,alongwiththesoundnessargumentinSec.3.WereportontheimplementationandevaluationoftheenhancedsynthesisinSec.4.Weconcludewithadiscussiononthelimitationsofread-onlyborrowsinSec.5paretorelatedworkinSec.6. 2ProgramSynthesiswithRead-OnlyBorrows WeintroducetheenhancementofSSLwithread-onlyborrowsbywalkingthereaderthroughaseriesofsmallbutcharacteristicexamplesofdeductivesynthesiswithseparationlogic.WeprovidethenecessarybackgroundonSSLinSec.2.1;thereadersfamiliarwiththelogicmaywanttoskiptoSec.2.2. 2.1BasicsofSSL-basedDeductiveProgramSynthesis InadeductiveSeparationLogic-basedsynthesis,aclientprovidesaspecificationofafunctionofinterestasapairofpre-andpost-conditions,suchas{P}voidfoo(locx,inti){Q}.ThepreconditionPconstrainsthesymbolicstatenecessarytorunthefunctionsafely(i.e.,withoutcrashes),whilethepostconditionQconstrainstheresultingstateattheendofthefunction’sexecution.AfunctionbodycsatisfyingtheprovidedspecificationisobtainedasaresultofderivingtheSSLstatement,representingthesynthesisgoal: {x,i};{P};{Q}|c Inthestatementabove,xandiareprogramvariables,andtheyareexplicitlystatedintheenvironmentΓ={x,i}.Variablesthatappearin{P}andthatarenotprogramvariablesarecalled(logical)ghostvariables,whilethenon-programvariablesthatonlyappearin{Q}arereferredtoas(logical)existentialones(EV).ThemeaningofthestatementΓ;{P};{Q}|cisthevalidityoftheHoare-styletriple{P}c{Q}forallpossiblevaluesofvariablesfromΓ.7Bothpre-andpostconditioncontainaspatialpartdescribingtheshapeofthesymbolicstate(spatialformulaearerangedoverviaP,Q,andR),andapurepart(rangedoverviaφ,ψ,andξ),whichstatestherelationsbetweenvariables(bothprogramandlogical).AderivationofanSSLstatementisconductedbyapplyinglogical 7Weoftencareonlyabouttheexistenceofaprogramctobesynthesised,notitsspecificshape.Inthosecaseswewillbeusingashorterstatement:Γ;{P};{Q}. 146A.Costeaetal. rules,whichreducetheinitialgoaltoatrivialone,soitcanbesolvedbyoneoftheterminalrules,suchas,e.g.,theruleEmpshownbelow: φ⇒ψEmpΓ;{φ;emp};{ψ;emp}|skip Thatis,Emprequiresthat(i)symbolicheapsinbothpre-andpost-conditionsareemptyand(ii)thatthepurepartφofthepreconditionimpliesthepurepartψofthepostcondition.Astheresult,Emp“emits”atrivialprogramskip.SomeoftheSSLrulesareaimedatsimplifyingthegoal,bringingittotheshapethatcanbesolvedwithEmp.Forinstance,considerthefollowingrules: FrameEV(Γ,
P,Q)∩Vars(R)=∅ Γ;{φ;P};{ψ;Q}|c Γ;{φ;P∗R};{ψ;Q∗R}|c UnifyHeaps[σ]R=R∅=dom(σ)⊆EV(Γ,
P,Q) Γ;{φ;P∗R};[σ]ψ;Q∗Rc Γ;{φ;P∗R};ψ;Q∗Rc NeitheroftherulesFrameandUnifyHeaps“adds”totheprogramcbeingsynthesised.However,FramereducesthegoalbyremovingamatchingpartR(a.k.a.frame)fromboththepre-andthepost-condition.UnifyHeapsnondeterministicallypicksasubstitutionσ,whichreplacesexistentialvariablesinasub-heapRofthepostconditiontomatchthecorrespondingsymbolicheapRintheprecondition.BothoftheserulesmakechoiceswithregardtowhatframeRtoremoveorwhichsubstitutionσtoadopt—apointthatwillbeofimportanceforthedevelopmentdescribedinSec.2.2. Finally,thefollowing(simplified)ruleforproducingamandisoperational,asitemitsapartoftheprogramtobesynthesised,whilealsomodifyingthegoalordingly.Theresultingprogramwill,thus,consistoftheemittedstore∗x=eofanexpressionetothepointervariablex.Theremainderissynthesisedbysolvingthesub-goalproducedbyapplyingtheWriterule. Vars(e)⊆Γe=eΓ;{φ;x→e∗P};{ψ;x→e∗Q}|c Write Γ;φ;x→e∗P;{ψ;x→e∗Q}∗x=e;c Asitmonwithproofsearch,shouldnoruleapplytoanintermediategoalwithinoneofthederivations,thedeductivesynthesisback-tracks,possiblydiscardingapartiallysynthesisedprogramfragment,tryingalternativederivationbranches.Forinstance,firingUnifyHeapstounifywrongsub-heapsmightleadthesearchdownapathtoanunsatisfiablegoal,eventuallymakingthesynthesisback-trackandleadingtolongersearch.ConsideralsoamisguidedapplicationofWriteintoacertainlocation,whichcancausethesynthesizertogeneratealessintuitiveprogramthat“makesup”fortheearlierspuriouswrites.Thisispreciselywhatwearegoingtofixbyintroducingread-onlyannotations. 2.2ReducingNon-DeterminismwithRead-OnlyAnnotations ConsiderthefollowingexampleadaptedfromtheoriginalSSLpaper[34].Whiletheexampleisintentionallyartificial,itcapturesafrequentsynthesisscenario—non-determinismduringsynthesis.Thisspecificationallowsacertaindegreeoffreedominhowitcanbesatisfied: ConciseRead-OnlySpecificationsforBetterSynthesis147 {x→239∗y→30}voidpick(locx,locy){z≤100;x→z∗y→z}
(4) ItseemslogicalforthesynthesistostarttheprogramderivationbyapplyingtheruleUnifyHeaps,thusreducingtheinitialgoaltotheoneoftheform {x,y};{x→239∗y→30};{239≤100;x→239∗y→239} Thisnewgoalhasbeenobtainedbypickingoneparticularsubstitutionσ=[239/z](outofmultiplepossibleones),whichdeliverstwoidenticalheapletsoftheformx→239inpre-andpostcondition.ItistimefortheWriteruletostriketofixthediscrepancybetweenthesymbolicheapinthepre-andpostconditionbyemittingmand∗y=239(atlast,someexecutablecode!
),andresultinginthefollowingnewgoal(noticethechangeofy-relatedentryintheprecondition): {x,y};{x→239∗y→239};{239≤100;x→239∗y→239} WhatfollowsaretwoapplicationsoftheFrameruletomonsymbolicheaps,leadingtothegoal:{x,y}{emp};{239≤100;emp}.Atthispoint,weareclearlyintrouble.Thepurepartofthepreconditionissimplytrue,whilethepostcondition’spurepartis239≤100,whichisunsolvable. Turnsoutthatourinitialpickofthesubstitutionσ=[239/z]wasanunfortunateone,andweshoulddiscardtheseriesofruleapplicationsthatfollowedit,back-trackandadoptadifferentsubstitution,e.g.,σ=[30/z],whichwillindeedresultinsolvingourinitialgoal.8 Letusnowconsiderthesamespecificationforpickthathasbeenenhancedbyexplicitlyannotatingpartsofthesymbolicheapasmutableandread-only: x→M239∗y→RO30voidpick(locx,locy)z≤100;x→Mz∗y→ROz
(5) InthisversionofSSL,theeffectofrulessuchasEmp,Frame,andUnifyHeapsremainsthesame,whileoperationalrulessuchasWrite,eannotationaware.Specifically,theruleWriteisnowreplacedbythefollowingone: Vars(e)⊆Γe=eΓ;φ;x→Me∗P;ψ;x→Me∗Qc WriteRO Γ;φ;x→Me∗P;ψ;x→Me∗Q∗x=e;c Noticehowintheruleabovetheheapletsoftheformx→MearenowannotatedwiththeesspermissionM,whichexplicitlyindicatesthatthecodemay modifythecorrespondingheaplocation.Followingwiththeexamplespecification
(5),wecanimagineasimilarscenario whentheruleUnifyHeapspicksthesubstitutionσ=[239/z].Shouldthisbethecase,thenextapplicationoftheruleWriteROwillnotbepossible,duetotheread-onlyannotationontheheaplety→RO239intheresultingsub-goal: {x,y};x→M239∗y→RO30;z≤100;x→M239∗y→RO239 AstheROesspermissionpreventsthesynthesisedcodefrommodifyingthegreyedheaplets,thesynthesissearchisforcedtoback-track,pickinganalternativesubstitutionσ=[30/z]andconvergingonthedesirableprogram∗x=30. 8Onemightarguethatitwaspossibletodetecttheunsolvableconjunct239≤100inthepostconditionimmediatelyafterperformingsubstitution,thussparingtheneedtoproceedwiththisderivationfurther.Thisis,indeed,apossibility,butingeneralitishardtoarguewhichoftheheuristicsinapplyingtheruleswillworkbetteringeneral.WedeferthequantitativeargumentonthismatteruntilSec.4.4. 148A.Costeaetal. 2.3ComposingRead-OnlyBorrows Havingsynthesisedthepickfunctionfromspecification
(5),wewouldliketouseitinfutureprograms.Forexample,imaginethatatsomepoint,whilesynthesisinganotherprogram,weseethefollowingasanintermediategoal: {u,v};u→M239∗v→M30∗P;w≤200;u→Mw∗v→Mw∗
Q
(6) Itisclearthat,modulothenamesofthevariables,wecansynthesiseapartofthedesiredprogrambyemittingacallpick(u,v),whichwecanthenreducetothegoal{u,v}{P};{w≤200;Q}viaanapplicationofFrame. Whyisemittingsuchacalltopick()safe?
Intuitively,thiscanbedonebecausethepreconditionofthespec(5)isweakerthantheoneinthegoal
(6).Indeed,thepreconditionofthelatterprovidesthefull(mutable)esspermissionontheheapportionv→M30,whilethepre/postconditionofformerrequiresaweakerformofess,namelyread-only:y→RO30.Therefore,ourlogicalfoundationsshouldallowtemporary“downgrading”ofanesspermission,e.g.,fromMtoRO,forthesakeofsynthesisingcalls.Whileallowingthisisstraightforwardandcanbedonesimilarlytoup-castingatypeinlanguageslikeJava,whatturnsouttobelesstrivialismakingsurethatthecaller’sinitialstrongeresspermission(M)isrestoredoncepick(u,v)returns. Non-solutions.Perhaps,thesimplestwaytoallowthecalltoafunctionwithaweaker(intermsofesspermissions)specification,wouldbeto(a)downgradethecaller’spermissionsonthecorrespondingheapfragmentstoRO,and(b)recoverthepermissionsasperthecallee’sspecification.Thisapproachsignificantlyreducestheexpressivityofthelogic(and,asaconsequence,pletenessofthesynthesis).Forinstance,adoptingthisstrategyforusingspecification(5)inthegoal(6)wouldresultintheunsolvablesub-goaloftheform{u,v};u→M30∗v→RO30∗P;u→M30∗v→M30∗
Q.Thisisduetothefactthat thepostconditionrequirestheheapletv→M30tohavethewrite-permissionM,whilethenewpreconditiononlyprovidestheess. Anotherwaytocaterforaweakercallee’sspecificationwouldbeto“chipout”aRO-permissionfromacaller’sM-annotation(inthespiritoffractionalpermissions),offerittothecallee,andthen“merge”itbacktothecaller’sfullblownpermissionuponreturn.Thissolutionworksforsimpleexamples,butnotforheappredicateswithmixedpermissions(discussioninSec.6).Yetanotherapproachwouldbetocreatea“ROclone”ofthecaller’sM-annotation,introducinganaxiomoftheformx→Mtx→Mt∗x→ROt.Theponentx→ROtcouldbeprovidedtothecalleeanddiscardeduponreturnsincethecallerretainedthefullpermissionoftheoriginalheap.SeveralworksonROpermissionshaveadoptedthisapproach[9,11,13].Whilediscardingsuchclonesworksjustfineforsequentialprogramverification,inthecaseofsynthesisguidedbypreandpostconditions,pletepostconditionscouldleadtointractablegoals. Oursolution.Thekeytogainingthenecessaryexpressivitywrt.passing/returningesspermissions,whilemaintainingasoundyetsimplelogic,istreatingesspermissionsasfirst-classvalues.Anaturalconsequenceofthistreatmentisthatimmutabilityannotationscanbesymbolic(i.e.,variablesofaspecialsort ConciseRead-OnlySpecificationsforBetterSynthesis149 “permission”),andthesemanticsofsuchvariablesiswellunderstood;werefertothesesymbolicannotationsasread-onlyborrows.9Forinstance,usingborrows,wecanrepresentthespecification(5)asanequivalentone: x→M239∗y→a30voidpick(locx,locy)z≤100;x→Mz∗y→az
(7) Theonlysubstantialdifferencewithspec(5)isthatnowthepointery’sesspermissionisgivenanexplicitnamea.Suchnamedannotations(a.k.a.borrows)aretreatedasRObythecallee,aslongasthepurepreconditiondoesnotconstrainthemtobemutable.However,givingthesepermissionsnamesachievesanimportantgoal:performingurateountingposingspecificationswithdifferentesspermissions.Specifically,wecannowemitacalltopick(u,v)asspecifiedby(7)fromthegoal
(6),keepinginmindthesubstitutionσ=[u/x,v/y,M/a].Thiscallnowountsforborrowsaswell,andmakesitstraightforwardtorestorev’soriginalpermissionMuponreturning. Followingthesameidea,borrowscanbeposedthroughcaptureavoidingsubstitutions.Forinstance,thesamespecification(7)ofpickcouldbeusedtoadvancethefollowingmodifiedversionofthegoal
(6): {u,v};u→M239∗v→c30∗P;w≤210;u→Mw∗v→cw∗
Q bymeansoftakingthesubstitutionσ=[u/x,v/y,c/a]. 2.4Borrow-PolymorphicInductivePredicates SeparationLogicowesitsglorytotheextensiveuseofinductiveheappredicates—pactwaytocapturetheshapeandthepropertiesoffiniteheapfragmentscorrespondingtorecursivelinkeddatastructures.Belowweprovideoneofthemostwidely-usedSLpredicates,definingtheshapeofaheapcontaininganullterminatedsingly-linkedlistwithelementsfromasetS: ls(x,S)x=0∧{S=∅;emp}
(8) |x=0∧{S={v}∪S1;[x,2]∗x→v∗x,1→nxt∗ls(nxt,S1)} Thepredicatecontainstwoclausesdescribingthecorrespondingcasesofthe list’sshapedependingonthevalueoftheheadpointerx.Ifxiszero,thelist’sheaprepresentationisempty,andsoisthesetofelementsS.Alternatively,ifxisnotzero,itstoresarecordwithtwoitems(indicatedbytheblockassertion [x,2]),suchthatthepayloadpointerxcontainsthevaluev(whereS={v}∪S1forsomesetS1),andthepointer,correspondingtox+1(denotedasx,1)containstheaddressofthelist’stail,nxt. Whileexpressiveenoughtospecifyandenablesynthesisofvariouslist-traversingandlist-generatingrecursivefunctionsviaSSL,thedefinition(8)doesnotallowonetorestricttheesspermissionstodiffponentsofthelist:alloftheinvolvedmemorylocationscanbemutated(whichexplainsthesynthesisissuewedescribedinSec.1.1).ToremedythisweaknessofthetraditionalSLstylepredicates,weproposetoparameterisethemwithread-onlyborrows,thusmakingthemawareofdifferentesspermissionstotheirponents.Forinstance,weproposetoredefinethelinkedlistpredicateasfollows: 9Inthisregard,oursymbolicborrowsareverysimilartoabstractfractionalpermissionsinChaliceandVeriFast[21,27].WediscusstherelationindetailinSec.6. 150A.Costeaetal. ls(x,S,a,b,c)x=0∧{S=∅;emp}|x=0∧S={v}∪S1;[x,2]a∗x→bv∗x,1→cnxt∗ls(nxt,S1,a,b,c)
(9) Thenewdefinition(9)issimilartotheoldone
(8),butnow,inadditiontothestandardpredicateparameters(i.e.,theheadpointerxandthesetSinthiscase),alsofeaturesthreeborrowparametersa,b,andcthatstandasplaceholdersfortheesspermissionstosomeponentsofthelist.Specifically,thesymbolicborrowsbandccontrolthepermissionstomanipulatethepointersxandx+1,correspondingly.Theborrowa,modifyingablocktypeheaplet,determineswhethertherecordstartingatxcanbedeallocatedwithfree(x).Allthethreeborrowsarepassedinthesameconfigurationtotherecursiveinstanceofthepredicate,therebyimposingthesameconstraintsontherestofthecorrespondingponents. Letusseetheborrow-polymorphicinductivepredicatesinaction.Considerthefollowingspecificationthatasksforafunctiontakingalistofarbitraryvaluesandreplacingallofthemwithzeroes:10 {ls(x,S,d,M,e)}voidreset(locx){ls(x,O,d,M,e)} (10) Thespec(10)givesverylittlefreedomtothefunctionthatwouldsatisfyitwithregardtopermissionstomanipulatethecontentsoftheheap,constrainedbythepredicatels(x,S,d,M,e).Asthefirstandthethirdborrowparametersareinstantiatedwithread-onlyborrows(dande),thedesiredfunctionisnotgoingtobeabletochangethestructuralpointersordeallocatepartsofthelist.Theonlyallowedmanipulationis,thus,changingthevaluesofthepayloadpointers. Thisconcisespecificationispleasantlystrong.Towit,inplainSSL,asimilarspec(withoutread-onlyannotations)wouldalsoadmitanimplementationthatfullydeallocatesthelistorarbitrarilychangesitslength.Inordertoavoidthesees,onewould,therefore,needtoprovideanalternativedefinitionofthepredicatels,whichwouldincorporatethelengthpropertytoo. Imaginenowthatonewouldliketousetheimplementationofresetsatisfyingspecification(10)togenerateafunctionwiththefollowingspec,providingstrongeresspermissionsfortheponents: {ls(y,
S,M,
M,M)}voidcall_reset(locy){ls(y,
O,M,
M,M)} Duringthesynthesisofcallreset,acalltoresetisgenerated.Forthispurposetheesspermissionsareborrowedandrecoveredasperspec(10)viathesubstitution[y/x,M/d,M/e]inawaydescribedinSec.2.3. 2.5PuttingItAllTogether WeconcludethisoverviewbyexplaininghowsynthesisviaSSLenhancedwithread-onlyborrowsavoidstheissuewithspuriouswritesoutlinedinSec.1.1. Tobegin,wechangethespecificationtothefollowingone,whichmakesuseofthenewlistpredicate(9)andpreventsanymodificationsintheoriginallist. r→Mx∗ls(x,S,a,b,c)listcopy(r)r→My∗ls(x,S,a,b,c)∗ls(y,
S,M,
M,M) Weshouldremarkthat,contrarytothesolutionsketchedattheendofSec.1.1,whichsuggestedusingthepredicateinstanceoftheshapels(x,S)[RO],ourconcreteproposaldoesnotallowustoconstraintheentirepredicatewithasingle 10WeuseOasanotationforamulti-setwithanarbitraryfinitenumberofzeroes. ConciseRead-OnlySpecificationsforBetterSynthesis151 Variablex,ySize,offsetn,ιExpressione::=Commandc::= Fun.dict.∆::= Alpha-numericidentifiersNon-negativeintegers0|true|x|e=e|e∧e|¬eletx=∗(x+ι)|∗(x+ι)=e|letx=malloc(n)|free(x)|err|f(ei)|c;c|if(e){c}else{c} |∆,f(xi){c} Fig.2:Programminglanguagegrammar. Puretermφ,ψ,χ,α::=0|true|M|RO|x|φ=φ|φ∧φ|¬φSymbolicheapP,
Q,R::=emp|e,ι→αe|[e,ι]α|p(φi)|P∗
Q HeappredicateD ::=p(xi)ek,{χk,Rk} FunctionspecF ::=f(xi):{P}{Q}AssertionP,Q::={φ;P} EnvironmentΓ :=|Γ,x ContextΣ:=|Σ,D|Σ,
F Fig.3:BoSSLassertionsyntax. esspermission(e.g.,RO).Instead,weallowfine-grainedesscontroltoitsparticularponentsbyannotatingeachonewithanindividualborrow.Thespecificationaboveallowsthegreatestflexibilitywrt.esspermissionstotheoriginallistbygivingthemdifferentnames(a,b,c). Intheprocessofsynthesisingthenon-trivialbranchoflistcopy,thesearchatsomepointeupwiththefollowingintermediategoal: {x,r,nxt,v,y12}; S={v}∪S1;r→My12∗[x,2]a∗x→bv∗x,1→cnxt∗ls(y12,S1,
M,M,M)∗... ;[z,2]M∗z→Mv∗z,1→My12∗ls(y12,S1,
M,M,M)∗... Sincethelogicalvariablezinthepostconditionisanexistentialone,thegreyedpartofthesymbolicheapcanbesatisfiedbyeither(a)re-purposingthegreyedpartoftheprecondition(whichiswhattheimplementationinSec.1.1does),or(b)allocatingacorrespondingrecordoftwoelements(asshouldbedone).Withtheread-onlyborrowsinplace,theunificationofthetwogreyedfragmentsinthepre-andpostconditionviaUnifyHeapsfails,becausethemutableannotationofz→Mvinthepostcannotbematchedbytheread-onlyborrowx→bvintheprecondition.Therefore,notbeingabletofollowthederivationpath(a),thesynthesiserisforcedtoexploreanalternativeone,eventuallyderivingtheversionoflistcopywithouttail-swapping. 3BoSSL:BorrowingSyntheticSeparationLogic WenowgiveaformalpresentationofBoSSL—aversionofSSLextendedwithread-onlyborrows.Fig.2andFig.3presentitsprogrammingandassertionlanguage,respectively.Forsimplicity,weformaliseacorelanguagewithouttheories(e.g.,naturalnumbers),similartotheoneofSmallfoot[6];theonlysortsinthecorelanguagearelocations,booleans,andpermissions(wherepermissionsappearonlyinspecifications)andthepurelogiconlyhasequality.Incontrast,ourimplementationsupportsintegersandsets(wherethelatteralsoonlyappearinspecifications),withlineararithmeticandstandardsetoperations.Wedo 152A.Costeaetal. WriteVars(e)⊆Γ e=e Γ;φ;x,ι→Me∗P;ψ;x,ι→Me∗Qc Γ;φ;x,ι→Me∗P;ψ;x,ι→Me∗Q∗(x+ι)=e;c ∗Alloc R=[z,n]α∗ 0≤iP,Q)=∅z∈EV(Γ,
P,Q) y,i→Mti Σ;Γ;φ;P∗R;{ψ;Q∗R}c Σ;Γ;{φ;P};{ψ;Q∗R}|lety=malloc(n);c ∗Free R=[x,n]M∗ 0≤i(3)findingasubstitutionσforR=[σ]PffailsifRdoesnothavesufficientessibilitypermissionstocallf(i.e.,substitutionsoftheforma/Maredisallowedsincethedomainofσmayonlycontainexistentials).Wereiteratethatread-onlyspecificationsonlymanipulatesymbolicborrows,thatistosay,ROconstantsarenotexpectedinthespecification. 3.2MemoryModel WecloselyfollowthestandardSLmemorymodel[32,37]andassumeLoc⊂Val. (Heap)h∈Heaps::=Loc→Val (Stack)s∈Stacks::=Var→Val ToenableC-likeountingofdynamically-allocatedmemoryblocks,weassumethattheheaphalsostoressizesofallocatedblocksindedicatedlocations.Conceptually,thispartoftheheapcorrespondstothemeta-dataofthememoryallocator.Thisountingensuresthatonlyapreviouslyallocatedmemoryblockcanbedisposed(asopposedtoanysetofallocatedlocations),enablingthemandtoeptasingleargument,theaddressoftheblock.Tomodelthismeta-data,weintroduceafunctionbl:Loc→Loc,wherebl(x)denotesthelocationintheheapwheretheblockmeta-datafortheaddressxisstored,ifxisthestartingaddressofablock.Inanactuallanguageimplementation,bl(x)mightbe,e.g.,x−1(i.e.,themeta-dataisstoredrightbeforetheblock). Sincewehaveoptedforanunsophisticatedpermissionmechanism,wheretheheapownershipisnotdivisible,butsomeheaplocationsarerestrictedtoRO,thedefinitionofthesatisfactionrelationΣ
I,RfortheannotatedassertionsinaparticularcontextΣandgivenaninterpretationI,isparameterisedwithafixedsetofread-onlylocations,R: –h,sΣ
I,R{φ;emp}iffφs=trueanddom(h)=∅. –h,s Σ,RI φ;e1,ι →αe2 iff φs=trueandl e1s+ιanddom(h)={l} andh(l)=e2sandl∈R⇔α=RO. – h,s Σ,
I R {φ ; [ e, n ] α } iff φs=trueandl bl(es)anddom(h)={l}and h(l)=nandl∈R⇔α=RO. –h,sΣ
I,R{φ;P1∗P2}iff∃h1,h2,h=h1∪·h2andh1,sIΣ,R{φ;P1}and h2,s Σ,
I R {φ ;
P 2 }. – h,s Σ,RI φ;p(ψi) iffφs=trueandD p(xi)ek,{χk,Rk}∈Σand h,ψis∈I(D)andk(h,sΣ
I,R[ψi/xi]{φ∧ek∧χk;Rk}). Therearetwonon-standardcases:points-toandblock,whosepermissionsmustagreewithR.Notethatinthedefinitionofsatisfaction,weonlyneedtoconsiderthatcasewherethepermissionαisavalue(i.e.,eitherROorM).Althoughinaspecificationαcanalsobeavariable,well-formednessguaranteesthatthisvariablemustbelogical,andhencewillbesubstitutedawayinthedefinitionofvalidity.WestressthefactthatareferencethathasROpermissionstoacertainsymbolicheapstillretainsthefullownershipofthatheap,withtherestrictionthatitisnotallowedtoupdateordeallocateit.Notethatdeallocationadditionallyrequiresamutablepermissionfortheenclosingblock. 154A.Costeaetal. 3.3Soundness TheBoSSLoperationalsemanticsisinthespiritofthetraditionalSL[38],andhenceisomittedforthesakeofsavingspace(selectedrulesareavailableintheextendedversionofthepaper).ThevaliditydefinitionandthesoundnessproofsofSSLareportedtoBoSSLwithoutanymodifications,sinceourcurrentdefinitionofsatisfactionimpliestheonedefinedforSSL: Definition1(Validity).Wesaythatawell-formedHoare-stylespecificationΣ;Γ;{P}c{Q}isvalidwrt.thefunctiondictionary∆iffwheneverdom(s)=Γ,∀σgv=[xi→di]xi∈GV(Γ,
P,Q)suchthath,sΣI[σgv]P,and∆;h,(c,s)·∗h,(skip,s)·,itisalsothecasethath,sΣI[σev∪·σgv]Qforsomeσev=[yj→dj]yj∈EV(Γ,
P,Q). Thefollowingtheoremguaranteesthat,givenaprogramcgeneratedwithBoSSL,aheapmodel,andasetofread-onlylocationsRthatsatisfytheprogram’sprecondition,executingcdoesnotchangethoseread-onlylocations: Theorem1(ROHeapsDoNotChange).GivenaHoare-stylespecificationΣ;Γ;{φ;P}c{Q},whichisvalidwrt.thefunctiondictionary∆,andasetofreadonlymemorylocationsR,if: (i)h,sΣ
I,R[σ]P,forsomeh,sandσ,and(ii)∆;h,(c,s)·∗h,(c,s)·forsomeh,sandc(iii)R⊆dom(h)thenR⊆dom(h)and∀l∈R,h(l)=h(l). Startingfromanabstractstatewhereaspatialheaphasaread-onlypermission,undernocircumstancecanthispermissionbestrengthenedtoM: Corollary1(NoPermissionStrengthening).GivenavalidHoare-stylespecificationΣ;Γ;{φ;P}c{ψ;Q}andapermissionα,ifψ⇒(α=M)thenitisalsothecasethatφ⇒(α=M). Asitturnsout,permissionweakeningispossible,since,thoughproblematic,postconditionweakeningissoundingeneral.However,eventhoughthisaffpleteness,itdoesnotaffectourterminationresults.Forexample,givenasynthesisedauxiliaryfunctionFf(x,r):x→a1t∗r→Mxx→a2t∗r→Mt+
1, andasynthesisgoalΣ,F;Γ;x→M7∗y→Mx;x→M7∗y→Mzc,firingtheCallruleforthecandidatefunctionf(x,r)wouldleadtotheunsolvablegoalΣ,F;Γ; x→a27∗y→M8;x→M7∗y→Mzf(x,y);c.Framemayneverbefiredonthis newgoalsincethepermissionofreferencexinthegoal’spreconditionhasbeenpermanentlyweakened.Toeliminatesuchsourcesofpletenesswerequiretheuser-providedpredicatesandspecificationstobewell-formed: Definition2(Well-FormednessofSpatialPredicates).Wesaythataspatialpredicatep(xi)ek,{χk,Rk}k∈1..Niswell-formediff (Nk=1(Vars(ek)∪Vars(χk)∪Vars(Rk))∩Perm)⊆(xi∩Perm). ConciseRead-OnlySpecificationsforBetterSynthesis155 Thatis,everyessibilityannotationwithinthepredicate’sclauseisboundbythepredicate’sparameters. Definition3(Well-FormednessofSpecifications).WesaythataHoarestylespecificationΣ;Γ;{P}c{Q}iswell-formediffEV(Γ,
P,Q)∩Perm=∅andeverypredicateinstanceinPandQisaninstanceofawell-formedpredicate. Thatis,postconditionsarenotallowedtohaveexistentialessibilityannotationsinordertoavoidpermanentweakeningofessibility. Acalleethatrequiresborrowsforasymbolicheapalwaysreturnsbacktothecalleritsoriginalpermissionforthatrespectivesymbolicheap: Corollary2(BorrowsAlwaysReturn).Aheapletwithpermissionα,either(a)retainsthesamepermissionαafteracalltoafunctionthatisdecoratedwithwell-formedspecificationsandthatrequiresforthatheaplettohaveread-onlypermission,or(b)itmaybedeallocatedincaseifα=
M. 4ImplementationandEvaluation WeimplementedBoSSLinanenhancedversionoftheSuSLiktool,whichwerefertoasROBoSuSLik[12].11ThechangestotheoriginalSuSLikinfrastructureaffectedlessthan100linesofcode.Theextendedsynthesisispatiblewiththeoriginalbenchmarks.Tomakethispossible,wetreattheoriginalSSLspecificationsasannotated/instantiatedwithMpermissions,whenevernecessary,whichisconsistentwithtreatmentofesspermissionsinBoSSL. WehaveconductedanextensiveexperimentalevaluationofROBoSuSLik,aimingtoanswerthefollowingresearchquestions:
1.DoborrowingannotationsimprovetheperformanceofSSL-basedsynthesis whenusingstandardsearchstrategy[34,§5.2]?

2.Doread-onlyborrowsimprovethequalityofsynthesisedprograms,intermsof sizeprehensibility,wrt.totheircounterpartsobtainedfromregular,“all-mutable”specifications?

3.DoweobtainstrongercorrectnessguaranteesfortheprogramsfromthestandardSSLbenchmarksuite[34,§6.1]bysimplyadding,wheneverreasonable,read-onlyannotationstotheirspecifications?

4.Doborrowingspecificationsenablemorerobustsynthesis?
Thatis,shouldweexpecttoobtainbetterprograms/synthesisperformanceonaverageregardlessoftheadoptedunificationandsearchstrategies?
4.1ExperimentalSetup BenchmarkSuite.Totackletheaboveresearchquestions,wehaveadoptedmostoftheheap-manipulatingbenchmarksfromSuSLiksuite[34,§6.1](withsomevariations)intooursetsofexperiments.Inparticularwelookedatthegroupofbenchmarkswhichmanipulatesinglylinkedlistsegments,sortedlinkedlistsegmentsandbinarytrees.Wedidnotincludethebenchmarksconcerningbinarysearchtrees(BSTs)forthereasonsoutlinedinthenextparagraph. 11Thesourcesareavailableat/TyGuS/robosuslik. 156A.Costeaetal. TheTools.ForaparisonwhichountsforthelatestadvancementstoSuSLik,wechosetoparameterisethesynthesisprocesswithaflagthatturnstheread-onlyannotationsonandoff(offmeansthattheyaresettobemutable).ThosevalueswhicharetheresultofhavingthisflagsetwillbemarkedintheexperimentswithRO,whilethosemarkedwithMutignoretheread-onlyannotationsduringthesynthesisprocess.Forsimplicity,wewillrefertothetwoinstancesofthetool,namelyROandMut,astwodifferenttools.Eachtoolwassettotimeoutafter2minutesofattemptingtosynthesiseaprogram. Criteria.Inanattempttoquantifyourresults,wehavelookedatthesizeofthesynthesisedprogram(ASTsize),theabsolutetimeneededtosynthesisethecodegivenitsspecification,averagedoverseveralruns(Time),thenumberofbacktrackingsintheproofsearchduetonondeterminism(#Backtr),thetotalnumberofruleapplicationsthatthesynthesisfiredduringthesearch(#Rules),includingthosethatleadtounsolvablegoals,andthestrengthoftheguaranteesofferedbythespecifications(StrongerGuarantees). Variables.Somebenchmarkshaveshownimprovementoverthesynthesisprocesswithouttheread-onlyannotations.Toemphasisethefactthatread-onlyannotations’improvementsarenotidental,wehavevariedtheinductivedefinitionsofthecorrespondingbenchmarkstoexperimentwithdifferentpropertiesoftheunderlyingstructure:theshapeofthestructure(inallthedefinitions),thelengthofthestructure(forthosebenchmarkstaggedwithlen),thevaluesstoredwithinthestructure(val),binationofalltheseproperties(all)aswellaswiththesortednesspropertyforthe“Sortedlist”groupofbenchmarks. ExperimentSchema.Tomeasuretheperformanceandthequalityoftheborrowingawaresynthesisweranthebenchmarksagainstthetwodifferenttoolsanddidaparisonoftheresults.Weraneachtoolthreetimesforeachbenchmark,andaveragetheresultedsynthesistime.Alltheotherevaluationcriteriaremainconstantwithinallthreeruns. Tomeasurethetools’robustnesswestressedthesynthesisalgorithmbyalteringthedefaultproofsearchstrategy.Weprepared42suchperturbationswhichweusedtorunagainstthedifferentprogramvariantsenumeratedabove.EachpairofprogramvariantandproofstrategyperturbationhasbeenthenanalysedtomeasurethenumberofrulesthathadbeenfiredbyROandMut. HardwareSetup.Theexperimentswereconductedona64-bitmachinerunningUbuntu,withanIntelXeonCPU(6cores,2.40GHz)with32GBRAM. 4.2PerformanceandQualityoftheBorrowing-AwareSynthesis Tab.1capturestheresultsofrunningROandMutagainsttheconsideredbenchmarks.Itprovidestheempiricalproofthattheborrowing-awaresynthesisimprovestheperformanceoftheoriginalSSL-basedsynthesis,orinotherwords,answeringpositivelytheResearchQuestion1.ROsuffersalmostnolossinperformance(exceptforafewcases,suchasthelistsegmentappendwherethereisanegligibleincreaseintime),whilethegainisconsiderableforthosesynthesisproblemsplexpointermanipulation.Forexample,ifweconsiderthenumberoffiredrulesastheperformancemeasurementcriteria,intheworst ConciseRead-OnlySpecificationsforBetterSynthesis157 GroupDescriptionASTsizeROMut append2020 delete 4444 dispose1111 Linked init 1313 List lcopy 3235 Segmentlength 2222 max 2828 min 2828 singleton1111 ins-sort-all2929 Sortedins-sort-len2929 Listins-sort-val2929 insert 5353 prepend1111 dispose1616 fl3535 flatten-app4848 morph1919 tcopy-all4251 tcopy-len3642 Treetcopy-val4251tcopy-ptr-all4655 tcopy-ptr-len4046 tcopy-ptr-val4655 tsize-all3238 tsize-len3232 tsize-ptr-all3642 tsize-ptr-len3636 Time(sec)ROMutMut/RO 1.51.41.92.10.50.50.70.71.01.01.51.51.41.51.51.50.50.53.73.83.03.02.62.57.88.00.50.60.40.52.12.01.61.70.60.51.52.21.32.01.45.31.62.41.32.21.35.81.51.41.21.11.61.41.31.3 0.9x1.1x1.0x1.0x1.0x1.0x1.1x1.0x1.0x1.0x1.0x1.0x1.0x1.2x1.2x1.0x1.0x1.0x1.5x1.5x3.8x1.5x1.7x4.5x0.9x0.9x0.9x1.0x #Backtr. #Rules Stronger ROMutMut/ROROMutMut/ROGuarant. 8867670055914222222885578553596110024241414111088690101222108869010122224222422 1.0x1.0x1.0x1.0x1.5x1.0x1.0x1.0x1.0x1.0x1.1x1.0x2.7x1.0x1.0x1.0x1.0x1.0x8.8x15x122x8.8x15x122x2.0x1.0x2.0x1.0x 7778180180 882727668238383838383830306060596057572143381717101011811876762424852967230482267393303803118926794551444653585253 1.0x1.0x1.0x1.0x1.2x1.0x1.0x1.0x1.0x1.0x1.0x1.0x1.6x1.0x1.0x1.0x1.0x1.0x3.5x4.2x32x3.3x3.9x30x1.1x1.0x1.1x1.0x YESsamesameYESYESYESYESYESsameYESYESYESYESYESsamesamesameYESYESYESYESYESYESYESYESYESYESYES Table1:Benchmarksparisonbetweentheresultsforsynthesiswithreadonlyannotations(RO)andwithoutthem(Mut).ForeachcasestudywemeasuretheASTsizeofthesynthesisedprogram,theTimeneededtosynthesizethebenchmark,thenumberoftimesthatthesynthesiserhadtodiscardaderivationbranch(#Backtr.),andthetotalnumberoffiredrules(#Rules). case,RObehavesthesameasMut,whileinthebestscenarioitbuysusa32-folddecreaseinthenumberofappliedrules.Atthesametime,synthesisingafewsmallexamplesintheROcaseisabitslower,despitethesameorsmallernumberofruleapplications.Thisisduetotheincreasednumberoflogicalvariables(becauseofaddedborrows)whendischargingobligationsviaSMTsolver. Fig.5offersastatisticalviewofthenumbersinthetable,wheresmallerbarsmarkabetterperformance.Thebarplotsindicatethatasplexityoftheproblemincreases(approximatelyfromlefttoright),ROoutperformsMut. Perhapsthemostimportanttake-awayfromthisexperimentisthatthesynthesiswithread-onlyborrowsoftenproducesamoreconciseprogram(lightgreencellsinthecolumntASTsizeofTab.1),whileretainingthesameorbetterperformancewrt.alltheevaluatedcriteria.Forinstance,ROgetsridofthespuriouswritefromthemotivatingexampleintroducedinSec.1,reducingtheASTsizefrom35nodesdownto32,whileinthesametimefiringfewerrules.ThatalsomeansthatwesecureapositiveanswerforResearchQuestion2. 4.3StrongerCorrectnessGuarantees ToanswerResearchQuestion3,wehaveparedtheguaranteesofferedbythespecificationsannotatedwithROpermissionsagainstthedefault 158A.Costeaetal. 60Read−Only 50 Mutable ASTSizesofSynthesisedPrograms NumberofASTNodes 40 30 20 10
0 ngthmaxminletonposeinitlcopypendeletependsertt−lent−valrt−all−lene−allr−lentr−allposeorph−leny−valy−allr−lenr−valtr−all−app− le singdis apdpreins−sors−sorns−sotsizetsizize−ptsize−pdismtcopytcoptcoppy−ptopy−ptopy−pflattenflatten inini tst tcotctc 10 Read−Only Mutable RulesTriedwhileSearching
8 log2ofnumberoftriedrules
6 4
2 0 ngthmaxminletonposeinitlcopypendeletependsertt−lent−valt−all−lene−allr−lentr−allposeorph−len−valy−allr−lenr−valtr−all−app− le singdis apdpreins−sors−sorns−sortsizetsizize−ptsize−pdismtcopytcopytcoppy−ptopy−ptopy−pflattenflatten inini tst tcotctc Fig.5:StatisticsforsynthesiswithandwithoutRead-Onlyspecifications. ones-theresultsaresummarizedinthelastcolumnofTab.1.Forinstance,aspecificationstatingthattheshapeofalinked-listsegmentisread-onlyimpliesthatthesizeofthatsegmentremainsconstantthroughtheprogram’sexecution.Inotherwords,thelengthpropertyneednotbecapturedseparatelyinthesegment’sdefinition.If,inadditiontotheshape,thepayloadofthesegmentisalsoread-only,thenthesetofvaluesandtheirorderingarealsoinvariant. Considerthegoal{lseg(x,y,s,a1,a2,a3)};{lseg(x,y,s,a1,a2,a3)},wherelsegisaninductivedefinitionofalistsegmentwhichendsatyandcontainsthesetofvaluess.Theborrowing-awaresynthesiserwillproduceaprogramwhichisguaranteedtotreatthesegmentpointedbyxandendingwithyasread-only(thatis,itsshape,length,valuesandorderingsareinvariant).Atthesametime,foragoal{lseg(x,y,s)};{lseg(x,y,s)},theguaranteesarethatthereturnedsegmentstillendsinyandcontainsvaluess.Internalmodificationsofthesegment,suchasreorderingandduplicatinglistelements,maystillur. ThefewentriesmarkedwithsameareprogramswithspecificationswhichhavenotgotstrongerwheninstrumentedwithROannotations(e.g.,delete).Thesebenchmarksrequiremutationovertheentiredatastructure,hencetheread-onlyannotationsdonotinfluencetheofferedguarantees.Overall,ourobservationsthatread-onlyannotationsofferstrongerguaranteesareinagreementwiththeworksonSL-basedprogramverification[9,13],butarepromotedheretothemorechallengingproblemofprogramsynthesis. ConciseRead-OnlySpecificationsforBetterSynthesis159 4.4RobustnessunderSynthesisPerturbations Thereisnosinglesearchheuristicsthatwillworkequallywellforanygivenspecification:foraparticularfixedsearchstrategy,asynthesisercanexhibitsuboptimalperformanceforsomegoals,whileconvergingquicklyonsomeothers.Byevaluatingrobustnesswrt.toROandMspecificationmethodologies,wearehopingtoshowthat,providedalargevarietyof“reasonable”searchheuristics,read-onlyannotationsdeliverbettersynthesisperformance“onaverage”. Forthissetofexperiments,wehavefocusedonfourcharacteristicprogramsfromourperformancebenchmarksbasedontheirpointerplexity:listsegmentcopy(lcopy),insertionintoasortedlistsegment(insert),copyingatree(tcopy),andavariationofthetreecopythatsharesthesamepointerfortheinputtreeanditsreturnedcopy(tcopy-ptr). ExploringDifferentUnificationOrders.Sincespatialunificationstaysatthecoreofthesynthesisprocess,weimplemented6differentstrategiesforchoosingaunificationcandidatebasedonthefollowingcriteria:thesizeoftheheapletchunk(favorthesmallestheapvs.thelargestoneasthebestunificationcandidate),thenameofthepredicate(weconsideredbothanascendingaswellasadescendingpriorityqueue),andacustomisedrankingfunctionwhichassociatesacosttoasymbolicheapbasedonitskind—ablockischeapertounifythanapoints-towhichinturnischeaperthanaspatialpredicate. ExploringDifferentSearchStrategies.Wenextdesigned6strategiesforprioritisingtheruleapplications.Oneofthecruxrulesinthismatter,istheWriterulewhosedifferentpriorityschemesmightmakealltheresultsseemrandomlygenerated.InthecaseswhereWriteleadstounsolvablegoals,onemightrightfullyarguethatROhasaclearadvantageoverMut(failfast).However,forthecaseswheremutationleadstoasolutionfaster,thenMutmighthaveanadvantageoverRO(solvefast).Becausethesearejustintuitiveobservations,andforfairnesssake,weexperimentedwithboththecaseswhereWritehasahighandalowpriorityinthequeueofrulephases[34,§5.2].Sincemostofthebenchmarksinvolverecursion,wealsochosetoshufflearoundtheprioritiesoftheOpenandCallrules.Again,wechosebetweenastackhighandabottomlowpriorityfortheserulestogiveafairchancetobothtools. Weconsideredbinationsofthe6unificationpermutationsandthe6rule-applicationpermutations(plusthedefaultone)toobtain42differentproofsearchperturbations.Wewillusethefollowingnotationinthenarrativebelow:–Sistheprisingthesynthesisproblems:lcopy,insert,tcopy,tcopy-ptr.–Visthesetofallspecificationvariations:len,val,all.–Kisthesetofall42possibletoolperturbations. Thedistributionsofthenumberofrulesfiredforeachtool(ROandMut)withthe42perturbationsoverthe4synthesisproblemswith3variantsofspecificationeach,thatis1008differentsynthesisruns,aresummarisedusingtheboxplotsinFig.6.Thereisaboxplotcorrespondingtoeachpairoftoolandsynthesisproblem.Intheidealcase,eachboxplotcontains126datapointscorrespondingtoabination(v,k)ofaspecificationvariationv∈Vandatoolperturbationk∈
K.Aboxplotisthedistributionofsuchdatabasedona 160A.Costeaetal. Read−OnlyMutable 16 14 12 log2ofnumberoftriedrules 10
8 6 (126)lcopy (126)lcopy insert(42) insert(42) (126)tcopy (108)tcopy tr(90)tcopy−p tr(84)tcopy−p Fig.6:Boxplotsofvariationsinlog2(numbersofappliedrules)forsynthesisperturbations.Numbersofdatapointsforeachexamplearegiveninparentheses. sixnumbersummary:minimum,firstquartile,median,thirdquartile,maximum,outliers.Forexample,theboxplotfortcopy-ptrcorrespondingtoROandcontaining90datapoints,readsasfollows:“thesynthesisprocessesfiredbetween64and256rules,withmostoftheprocessesfiringbetween64and128rules.Therearethreeexceptionwherethesynthesiserfiredmorethan256rules”.Notethatthey-axisrepresentsthebinarylogarithmofthenumberoffiredrules. Eventhoughweattemptedtosynthesiseeachprogram126timesforeachtool,someattemptshitthetimeoutandthereforetheircorrespondingdatapointshadtobeeliminatedfromtheboxplot.Itisofnote,though,thatwheneverROwithconfiguration(v,k)hitthetimeoutforthesynthesisproblems∈S,sodidMut,henceboththe(RO,s,(v,k))aswellas(Mut,s,(v,k))areomittedfromtheboxplots.Buttheinversedidnothold:ROhitthetimeoutfewertimesthanMut,henceROismeasuredatdisadvantage(i.e.,moredatapointsmeansmoreopportunitiestoshowworseresults).Sinceinsertcollectedthehighestnumberoftimeouts,weequalisedittoremovenon-matchedentriesacrossthetwotools. DespiteRO’spotentialmeasurementdisadvantage,theboxplotsdepictsitasaclearwinner.NotonlyROfiresfewerrulesinallthecases,butwiththeexceptionofinsert,itisalsomorestabletotheproofsearchperturbations,itvariesafeworderofmagnitudelessthanMutdoesforthesameconfigurations.Fig.7supportsthisobservationbyofferingamoredetailedviewonthedistributionsofthenumbersoffiredrulespersynthesisconfiguration.Tallerbarsshowthatmoreprocessesfallinthesamerange(wrt.thenumberoffiredrules).Forlcopy,tcopy,tcopy-ptritisclearthatMuthasawiderdistributionofthenumberoffiredrules,thatis,MutismoresensitivetotheperturbationsthanRO.Weadditionallymakesomefurtherobservations: 60 lcopy(RO)126datapointslcopy(RO)126datapoints ConciseRinseerat(RdO-)OnlySpecifiopsy(RfOo)rBetterSynthetcsoipsy−ptr(RO)161 60 60 60 42datapoints 126datapoints 90datapoints insert(RO)42datapoints tcopy(RO)126datapoints tcopy−ptr(RO)90datapoints 10020103020403050406050 10020103020403050406050 10020103020403050406050 10020103020403050406050 FrequencyFrequency
0 4681012141618 4681012141618lcopy(Mut)126datapointslcopy(Mut)126datapoints 60
0 4681012141618 4681012141618insert(Mut)42datapointsinsert(Mut)42datapoints 60
0 4681012141618 4681012141618tcopy(Mut)108datapointstcopy(Mut)108datapoints 60
0 4681012141618 4681012141618tcopy−ptr(Mut)84datapointstcopy−ptr(Mut)84datapoints 60 10020103020403050406050 10020103020403050406050 10020103020403050406050 10020103020403050406050 FrequencyFrequency 4681012141618 4681012141618 4681012141618 4681012141618
0 0
0 0 4F6ig8.170:12D1i4st16ri1b8ution4s6of8lo10g212(numb141618erof4at6te8m10pt12ed14r16ul18eappl4ica6ti8on10s1)2.141618 –Despiteasimilardistributionwrt.thenumbersoffiredrulesinthecaseofinsert,ROpactASTsofsize53forallperturbations,whileMutfluctuatesbetweenproducingASTsofsize53and62. –Forallthesynthesistasks,ROproducedthesameASTirrespectiveofthetool’sperturbation.Incontrast,thereweresynthesisproblemsforwhichMutproducedasmanyas3differentASTsfordifferentperturbations,noneofwhichwereasconciseastheoneproducedbyROforthesameconfiguration. –Theoutliersof(Mut,lcopy)areridiculouslyhigh,firingcloseto40krules.–Theoutliersof(RO,tcopy)arestillbelowthemedianvaluesof(Mut,tcopy).–Exceptforinsert,thebestperformanceofMut,intermsoffiredrules,barely overlapswiththeworstperformanceofRO.–Exceptforinsert,themediansofROareclosertothelowestvalueofthe datadistribution,asopposedtoMutwherethetendancyistofiremorerules.–Inabsolutevalues,ROhitthe2-minutestimeout102paredtoMut, whichhitthetimeout132times. Webelievethatthemaintake-awaysfromthissetofexperiments,alongwiththepositiveanswertotheResearchQuestion4,areasfollows:–ROismorestablewrt.thenumberofrulesfiredandthesizeofthegenerated ASTformanyreasonableproofsearchperturbations.–ROproducesbetterprograms,whichavoidspuriousstatements,irrespective oftheperturbationandnumberofrulesfiredduringthesearch. 5LimitationsandDiscussion Flexiblealiasing.Separatingconjunctionassertsthattheheapcanbesplitintotwodisjointparts,orinotherwordsitcarriesanimplicitnon-aliasinginformation.Specifically,x→∗y→statesthatxandyarenon-aliased.Such 162A.Costeaetal. assertionscanbeusedtospecifymethodsasbelow: {x→n∗y→m∗ret→x}sum(x,y,ret){x→n∗y→m∗ret→n+m} asionally,enforcingxandytobenon-aliasedistoorestrictive,rejectingsafecallssuchassum(p,p,q).Approachestosupportimmutableannotationspermitsuchcallspromisingsafetyifbothpointers,aliasedornot,areannotatedasread-only[9,13].BoSSLdoesnotsupportsuchflexiblealiasing.Preconditionstrengthening.Letusassumethatsrtl(x,n,lo,hi,α
1,α2,α3)isaninductivepredicatethatdescribesasortedlinkedlistofsizenwithloandhibeingthelist’sminimumandmaximumpayloadvalue,respectively.Now,considerthefollowingsynthesisgoal: {x,y};{y→x∗srtl(x,n,lo,hi,
M,M,M)};{y→n∗srtl(x,n,lo,hi,
M,M,M)}.Asstated,thegoalclearlyrequirestheprogramputethelengthnofthelist.Imaginethatwealreadyhaveafunctionthatdoespreciselythat,eventhoughitisstatedintermsofalistpredicatethatdoesnotenforcesortedness: {ret→x∗ls(x,n,a1,a2,a3)}length(x,ret){ret→n∗ls(x,n,a1,a2,a3)} Tosolvetheinitialgoal,thesynthesisercouldweakenthegivenpreconditionsrtl(x,n,lo,hi,
M,M,M)tols(x,n,
M,M,M),andthenessfullysynthesiseacalltothelengthmethod.Unfortunately,theresultinggoal,obtainedafterhavingemittedthecalltolengthandapplyingFrame,isunsolvable: {x,y}{ls(x,n,
M,M,M)};{srtl(x,n,lo,hi,
M,M,M)}.sincethelogicdoesnotallowtostrengthenanarbitrarylinkedlisttoasortedlinkedlistwithoutretainingthepriorknowledge.Shouldwehaveadoptedanalternativeapproachtoread-onlyannotations[9,13]allowingthecallertoretainthefullpermissionofthesortedlist,thenthepostconditionoflengthwouldnotcontainthelist-relatedpartoftheheapandwouldonlyquantifyovertheresultpointer{ret→n},thusleadingtothesolvablegoalbelow: {x,y};{srtl(x,n,lo,hi,
M,M,M)};{srtl(x,n,lo,hi,
M,M,M)}. OnestraightforwardwayforBoSSLtocopewiththislimitationistosimplyaddaversionoflengthannotatedwithspecificationsthatcatertosrtl. ingthelimitations.Whilethe“callerkeepsthepermission”kindofapproachwouldbuyusflexiblealiasingandcallswithweakerspecifications,itpromisethebenefitsdiscussedearlierwithrespecttothegranularityofborrow-polymorphicinductivepredicates.Onepossiblesolutiontogainthebestofbothworldswouldbetodesignapermissionsystemwhichallowsbothborrow-polymorphicinductivepredicatesaswellasread-onlymodalitiestoco-exist,wherethelatterwouldoverwritethepredicate’smixedpermissions.Inotherwords,theread-onlymodalityenforcesaread-onlytreatmentofthepredicateirrespectiveofitspermissionarguments,whilethepermissionargumentscontrolthetreatmentofamutablepredicate.Thetheoreticalimplicationsofsuchadesignchoiceareleftaspartoffuturework. Extendingread-onlyspecificationstoconcurrency.Thusfarwehaveonlyinvestigatedthesynthesisofsequentialprograms,forwhichread-onlyannotationshelpedtoreducethesynthesiscost.Assumingthatthesynthesiserhasthecapabilitytosynthesiseconcurrentprogramsaswell,theborrowsannotationmechanisminitscurrentformmaynotbeabletocopewithgeneralresourcesharing. ConciseRead-OnlySpecificationsforBetterSynthesis163 Thisisbecauseacalleewhichrequiresread-onlypermissionstoaparticularsymbolicheapstillconsumestheentirerequiredsymbolicheapfromthecaller,despitetheread-onlyrequirement;hence,thereisnospaceleftforsharing.Thatsaid,therecentlyproposedalternativeapproachestointroduceread-onlyannotations[9,13]havenoformalsupportforheapsharinginthepresenceofconcurrencyeither.Toaddressthesechallenges,wecouldadoptamoresophisticatedapproachbasedonfractionalpermissionsmechanism[7,8,20,25,30],butthisisleftaspartoffutureworksinceitisorthogonaltothecurrentscope. 6RelatedWork Languagedesign.Thereisalargebodyofworkonintegratingesspermissionsintopracticaltypesystems[5,16,42](see,e.g.,thesurveybyClarkeetal.[10]).Onenotablesuchsystem,whichistheclosestinitsspirittoourproposal,istheborrowstypesystemoftheRustprogramminglanguage[1]provedsafewithRustBelt[22].Similartoourapproach,borrowsinRustareshort-lived:inRusttheysharethescopewiththeowner;inourapproachtheydonotescapethescopeofamethodcall.Incontrastwithourwork,Rust’stypesystemcarefullymanagesdifferentreferencestodatabyimposingstrictsharingconstraints,whereasinourapproachthetreatmentofaliasingistakencareofautomaticallybybuildingonSeparationLogic.Moreover,Rustallowsread-onlyborrowstobeduplicated,whileinthesequentialsettingofBoSSLthisiscurrentlynotpossible. Somewhatrelatedtoourapproach,Nadenetal.proposeamechanismsforborrowingpermissions,albeitintegratedasafundamentalpartofatypesystem[31].Theirtypeesequippedwithchangepermissionswhichenforcetheborrowingrequirementsanddescribetheeffectsoftheborrowinguponreturn.Asaresultoftreatingpermissionsasfirst-classvalues,wedonotneedtoexplicitlydescribetheflowofpermissionsforeachborrowsincethisiscontrolledbyamixofthesubstitutionandunificationprinciples. Programverificationwithread-onlypermissions.Boylandintroducedfractionalpermissionstostaticallyreasonaboutinterferenceinthepresenceofsharedmemoryconcurrency[8].Apermissionpdenotesfullresourceownership(i.e.read-writeess)whenp=1,whilep∈(0,1)denotesapartialownership(i.e.read-onlyess).Toleveragepermissionsinpractice,asystemmustsupporttwokeyoperations:permissionsplittingandpermissionborrowing.Permissionsplitting(andmergingback)followsthesplitrule:x→pa=x→p1a∗x→p2a,withp=p1+p2andp,p1,p2∈(0,1].Permissionborrowingreferstothesafemanipulationofpermissions:acalleemayremovesomepermissionsfromthecaller,usethemtemporarily,andgivethembackuponreturn. Thoughitexists,toolsupportforfractionalpermissionsisstillscarce.LeinoandMu¨llerintroducedamechanismforstoringfractionalpermissionsindatastructuresviadedicatedesspredicatesintheChaliceverificationtool[27].Topromotegenericspecifications,Heuleetal.advancedChalicewithinstatiableabstractpermissions,allowingautomaticfireofthesplitruleandsymbolicborrowing[20].VeriFast[21]isguidedbycontractswritteninSeparationLogicandassumestheexistenceoflemmastocaterforpermissionsplitting.Viper[30] 164A.Costeaetal. isanintermediatelanguagewhichsupportsvariouspermissionmodels,includingabstractfractionalpermissions[4,43].SimilartoChalice,thepermissionsareattachedtomemorylocationsusinganessibilitypredicate.Toreasonaboutit,Viperusespermission-awareassertionsandassumptions,whichcorrespondinourapproachtotheunificationandthesubstitutionoperations,respectively.LikeViper,weenhancethebasicmemoryconstructors,thatisblocksandpoints-to,toountforpermissions,butincontrast,theCallruleinourapproachisstandard,i.e.,notpermission-aware. Thesetools,alongwithothers[3,18],offerstrongcorrectnessguaranteesinthepresenceofresourcesharing.However,thereisaclassofproblems,namelythoseinvolvingpredicateswithmixedpermissions,whoseguaranteesareweakenedduetothegeneralfractionalpermissionsmodelbehindthesetools.Wenextexemplifythisclassofproblemsinasequentialsetting.Westartbyconsideringamethodwhichresetsthevaluesstoredinalinked-listwhilemaintainingitsshape(p<1belowistoenforcetheimmutableshape): {p<1;ls(x,S)[1,p]}voidreset(locx){ls(x,{0})[1,p]}.Assumeacalltothismethod,namelyreset(y).Thecallerhasfullpermissionovertheentirelistpassedasargument,thatisls(y,B)[1,1].Thisattemptleadstotwoissues.Thefirsthastodowithsplittingthepayload’spermission(beforethecall)suchthatitmatchesthecallee’spostcondition.Tobeabletomodifythelist’spayload,thecalleemustgetthepayload’sfullownership,hencethecallershouldretain0:ls(y,B)[1,1]=ls(y,B)[0,1/2]∗ls(y,B)[1,1/2].But0isnotavalidfractionalpermission.Thesecondissuesurfaceswhileattemptingtomergethepermissionsafterthecall:ls(y,B)[0,1/2]∗ls(y,{0})[1,1/2]isinvalidsincethetwoinstancesoflshavepatiblearguments(namelyBand{0}).Toavoidsuchproblems,BoSSLabandonsthesplitruleandinsteadalwaysmanipulatesfullownershipofresources,henceitdoesnotusefractions.promise,alongwiththesupportforsymbolicborrows,allowsROBoSuSLiktoguaranteereadonly-nessinasequentialsettingwhileavoidingtheaforementionedissues.Moreinvestigationsareneededinordertoliftthisresulttoconcurrencyreasoning.Anotherfeaturewhichdistinguishesthecurrentworkfromthosebasedonfractionalpermissions,isthesupportforpermissionsasparametersofthepredicate,whichinturnsupportsthedefinitionofpredicateswithmixedpermissions. ImmutablespecificationsofSeparationLogichavealsobeenstudiedbyDavidandChin[13].Unlikeourapproachwhichtreatsborrowsaspolymorphicvariablesthatrelyonthebasicconceptofsubstitution,theirannotationprisesonlyconstantsandrequiresaspeciallytailoredentailmentofenhancedproofrules.Sincecallersretaintheheapownershipuponcallingamethodwithread-onlyrequirements,theirmachinerysupportsflexiblealiasingandcut-pointpreservation—featuresthatwecouldnotfindagooduseforinthecontextofprogramsynthesis.AnattempttoextendDavidandChin’sworkbyaddingsupportforpredicateswithmixedpermissions[11]suffersfromsignificantannotationoverhead.Specifically,itemploysamixofmutable,immutable,andabsentpermissions,sothateachmutableheapletinthepreconditionrequiresacorrespondingmatchingheapletannotatedwithabsentinthepostcondition. ConciseRead-OnlySpecificationsforBetterSynthesis165 Chargu´eraudandPottier[9]extendedSeparationLogicwithROassertionsthatcanbefreelyduplicatedordiscarded.TheirapproachcreateslexicallyscopedcopiesoftheRO-permissionsbeforeemittingacall,which,inturn,involvesdiscardingthecorrespondingheapfromthepostconditiontoguaranteeasoundRO-modality.AdaptingthismodalitytoprogramsynthesisguidedbypreandpostconditionswouldrequirepletelynewsystemofdeductivesynthesissincemostoftherulesinSSLarenotdesignedtohandlethediscardableROheaps.Incontrast,BoSSLsupportspermission-parametricpredicates(e.g.,
(9))requiringonlyminimaladjustmentstoitshostlogic,i.e.,SSL. Programsynthesis.BoSSLcontinuesalonglineofworkonprogramsynthesisfromformalspecifications[26,36,40,41,44]andinparticular,deductivesynthesis[14,23,29,33,34],whichcanbecharacterisedassearchinthespaceofproofsofprogramcorrectness(ratherthaninthespaceofprograms).MostdirectlyBoSSLbuildsuponourpriorworkonSSL[34]andenhancesitsspecificationlanguagewithread-onlyannotations.Inthatsense,thepresentworkisalsorelatedtovariousapproachesthatusenon-functionalspecificationsasinputtosynthesis.Itmontousesyntacticnon-functionalspecifications,suchasgrammars[2],sketches[36,40],orrestrictionsonthenumberoftimesponentcanbeused[19].Morerecentworkhasexploredsemanticnon-functionalspecifications,includingtypeannotationsforresourceconsumption[24]andsecurity/privacy[17,35,39].Thisresearchdirectionispromisingbecause(a)annotationsoftenenabletheprogrammertoexpressastrongspecificationconcisely,and(b)checkingannotationsisoftenpositional(i.e.,failsfaster)thancheckingfunctionalspecifications,whichmakessynthesismoreefficient.Inthepresentworkwehavedemonstratedthatbothofthesebenefitsofnon-functionalspecificationsalsoholdfortheread-onlyannotationsofBoSSL. 7Conclusion Inthiswork,wehaveadvancedthestateoftheartinprogramsynthesisbyhighlightingthebenefitsofguidingthesynthesisprocesswithinformationaboutmemoryesspermissions.WehavedesignedthelogicBoSSLandimplementedthetoolROBoSuSLik,showingthataminimalisticdisciplineforread-onlypermissionsalreadybringssignificantimprovementswrt.theperformanceandrobustnessofthesynthesiser,aswellaswrt.thequalityofitsgeneratedprograms. Acknowledgements.WethankAlexanderJ.Summers,CristinaDavid,OlivierDanvy,andPeterO’Hearnformentsontheprelimiaryversionsofthepaper.WeareverygratefultotheESOP2020reviewersfortheirdetailedfeedback,whichhelpedtoconductamoreparisonwithrelatedapproachesand,thus,betterframetheconceptualcontributionsofthiswork. NadiaPolikarpova’sresearchwassupportedbyNSFgrant1911149.AmyZhu’sresearchinternshipandstayinSingaporeduringtheSummer2019wassupportedbyIlyaSergey’sstart-upgrantatYale-NUSCollege,andmadepossiblethankstoUBCScienceCo-opProgram. 166A.Costeaetal. References
1.TheRustProgrammingLanguage:ReferencesandBorrowing./1.8.0/book/references-and-borrowing.html,2019.
2.RajeevAlur,RastislavBod´ık,GarvitJuniwal,MiloM.K.Martin,MukundRaghothaman,SanjitA.Seshia,RishabhSingh,ArmandoSolar-Lezama,EminaTorlak,andAbhishekUdupa.Syntax-guidedsynthesis.InFMCAD,pages1–
8.IEEE,2013.
3.AndrewW.Appel.Verifiedsoftwaretoolchain-(invitedtalk).InESOP,volume6602ofLNCS,pages1–17.Springer,2011.
4.VytautasAstrauskas,PeterMu¨ller,FedericoPoli,andAlexanderJ.Summers.LeveragingRusttypesformodularspecificationandverification.PACMPL,3(OOPSLA):147:1–147:30,2019.
5.ThibautBalabonski,Fran¸coisPottier,andJonathanProtzenko.TheDesignandFormalizationofMezzo,aPermission-BasedProgrammingLanguage.ACMTrans.Program.Lang.Syst.,38
(4):14:1–14:94,2016.
6.JoshBerdine,CristianoCalcagno,andPeterW.O’Hearn.Symbolicexecutionwithseparationlogic.InAPLAS,volume3780ofLNCS,pages52–68.Springer,2005.
7.RichardBornat,CristianoCalcagno,PeterW.O’Hearn,andMatthewJ.Parkinson.PermissionountinginSeparationLogic.InPOPL,pages259–270.ACM,2005.
8.JohnBoyland.CheckingInterferencewithFractionalPermissions.InSAS,volume2694ofLNCS,pages55–72.Springer,2003.
9.ArthurChargu´eraudandFranc¸oisPottier.TemporaryRead-OnlyPermissionsforSeparationLogic.InESOP,volume10201ofLNCS,pages260–286.Springer,2017. 10.DaveClarke,JohanO¨stlund,IlyaSergey,andTobiasWrigstad.OwnershipTypes:ASurvey,pages15–58.SpringerBerlinHeidelberg,2013. 11.AndreeaCostea,AsankhayaSharma,andCristinaDavid.HIPimm:verifyinggranularimmutabilityguarantees.InPEPM,pages189–194.ACM,2014. 12.AndreeaCostea,AmyZhu,NadiaPolikarpova,andIlyaSergey.ROBoSuSLik:ESOP2020Artifact.2020.DOI:10.5281/zenodo.3630044. 13.CristinaDavidandWei-NganChin.Immutablespecificationsformoreconciseandpreciseverification.InOOPSLA,pages359–374.ACM,2011. 14.BenjaminDelaware,Cl´ementPit-Claudel,JasonGross,andAdamChlipala.Fiat:DeductiveSynthesisofAbstractDataTypesinaProofAssistant.InPOPL,pages689–700.ACM,2015. 15.RobertDockins,AquinasHobor,andAndrewW.Appel.Afreshlookatseparationalgebrasandshareounting.InAPLAS,volume5904ofLNCS,pages161–177.Springer,2009. 16.RonaldGarcia,E´ricTanter,RogerWolff,andJonathanAldrich.Foundationsoftypestate-orientedprogramming.ACMTrans.Program.Lang.Syst.,36
(4):12:1–12:44,2014. 17.Adri`aGasco´n,AshishTiwari,BrentCarmer,andUmangMathur.Lookfortheprooftofindtheprogram:ponent-basedprogramsynthesis.InCAV,volume10427ofLNCS,pages86–103.Springer,2017. 18.ColinS.Gordon,MatthewJ.Parkinson,JaredParsons,AleksBromfield,andJoeDuffy.Uniquenessandreferenceimmutabilityforsafeparallelism.InOOPSLA,pages21–40.ACM,2012. 19.SumitGulwani,SusmitJha,AshishTiwari,andRamarathnamVenkatesan.Synthesisofloop-freeprograms.InPLDI,pages62–73.ACM,2011. ConciseRead-OnlySpecificationsforBetterSynthesis167 20.StefanHeule,
K.RustanM.Leino,PeterMu¨ller,andAlexanderJ.Summers.Abstractreadpermissions:Fractionalpermissionswithoutthefractions.InVMCAI,volume7737ofLNCS,pages315–334.Springer,2013. 21.BartJacobs,JanSmans,PieterPhilippaerts,Fr´ed´ericVogels,WillemPenninckx,andFrankPiessens.VeriFast:APowerful,Sound,Predictable,FastVerifierforCandJava.InNASAFormalMethods,volume6617ofLNCS,pages41–55.Springer,2011. 22.RalfJung,Jacques-HenriJourdan,RobbertKrebbers,andDerekDreyer.RustBelt:SecuringthefoundationsoftheRustprogramminglanguage.PACMPL,2(POPL):66,2017. 23.EtienneKneuss,IvanKuraj,ViktorKuncak,andPhilippeSuter.Synthesismodulorecursivefunctions.InOOPSLA,pages407–426.ACM,2013. 24.TristanKnoth,DiWang,NadiaPolikarpova,andJanHoffmann.Resource-guidedprogramsynthesis.InPLDI,pages253–268.ACM,2019. 25.XuanBachLeandAquinasHobor.Logicalreasoningfordisjointpermissions.InESOP,volume10801ofLNCS,pages385–414.Springer,2018. 26.K.RustanM.LeinoandAleksandarMilicevic.ProgramExtrapolationwithJennisys.InOOPSLA,pages411–430.ACM,2012. 27.K.RustanM.LeinoandPeterMu¨ller.ABasisforVerifyingMulti-threadedPrograms.InESOP,volume5502ofLNCS,pages378–393.Springer,2009. 28.K.RustanM.Leino,PeterMu¨ller,andJanSmans.VerificationofConcurrentProgramswithChalice.InFoundationsofSecurityAnalysisandDesignV,FOSAD2007/2008/2009TutorialLectures,volume5705ofLNCS,pages195–222.Springer,2009. 29.ZoharMannaandRichardJ.Waldinger.Adeductiveapproachtoprogramsynthesis.ACMTrans.Program.Lang.Syst.,2
(1):90–121,1980. 30.PeterMu¨ller,MalteSchwerhoff,andAlexanderJ.Summers.Viper:AVerificationInfrastructureforPermission-BasedReasoning.InVMCAI,volume9583ofLNCS,pages41–62.Springer,2016. 31.KarlNaden,Roberthino,JonathanAldrich,andKevinBierhoff.Atypesystemforborrowingpermissions.InPOPL,pages557–570.ACM,2012. 32.PeterW.O’Hearn,JohnC.Reynolds,andHongseokYang.Localreasoningaboutprogramsthatalterdatastructures.InCSL,volume2142ofLNCS,pages1–19.Springer,2001. 33.NadiaPolikarpova,IvanKuraj,andArmandoSolar-Lezama.Programsynthesisfrompolymorphicrefinementtypes.InPLDI,pages522–538.ACM,2016. 34.NadiaPolikarpovaandIlyaSergey.StructuringtheSynthesisofHeapManipulatingPrograms.PACMPL,3(POPL):72:1–72:30,2019. 35.NadiaPolikarpova,JeanYang,ShacharItzhaky,andArmandoSolar-Lezama.Enforcinginformationflowpolicieswithtype-targetedprogramsynthesis.CoRR,abs/1607.03445,2016. 36.XiaokangQiuandArmandoSolar-Lezama.Naturalsynthesisofprovably-correctdata-structuremanipulations.PACMPL,1(OOPSLA):65:1–65:28,2017. 37.JohnC.Reynolds.Separationlogic:Alogicforsharedmutabledatastructures.InLICS,pages55–74.IEEEComputerSociety,2002. 38.ReubenN.S.RoweandJamesBrotherston.Automaticcyclicterminationproofsforrecursiveproceduresinseparationlogic.InCPP,pages53–65.ACM,2017. 39.CalvinSmithandAwsAlbarghouthi.Synthesizingdifferentiallyprivateprograms.Proc.ACMProgram.Lang.,3(ICFP):94:1–94:29,July2019. 40.ArmandoSolar-Lezama.Programsketching.STTT,15(5-6):475–495,2013. 168A.Costeaetal.41.SaurabhSrivastava,SumitGulwani,andJeffreyS.Foster.Fromprogramverifica- tiontoprogramsynthesis.InPOPL,pages313–326.ACM,2010.42.SvenStork,KarlNaden,JoshuaSunshine,ManuelMohr,AlcidesFonseca,Paulo Marques,andJonathanAldrich.Æminium:APermission-BasedConcurrent-byDefaultProgrammingLanguageApproach.TOPLAS,36
(1):2:1–2:42,2014.43.AlexanderJ.SummersandPeterMu¨ller.Automatingdeductiveverificationforweak-memoryprograms.InTACAS,volume10805ofLNCS,pages190–209.Springer,2018.44.EminaTorlakandRastislavBod´ık.Alightweightsymbolicvirtualmachineforsolver-aidedhostlanguages.InPLDI,pages530–541.ACM,2014. OpenessThischapterislicensedunderthetermsoftheCreativeCommonsAttribution4.0InternationalLicense(/licenses/by/4.0/),whichpermitsuse,sharing,adaptation,distributionandreproductioninanymediumorformat,aslongasyougiveappropriatecredittotheoriginalauthor(s)andthesource,providealinktotheCreativeCommonslicenseandindicateifchangesweremade. Theimagesorotherthirdpartymaterialinthischapterareincludedinthechapter’sCreativeCommonslicense,unlessindicatedotherwiseinacreditlinetothematerial.Ifmaterialisnotincludedinthechapter’sCreativeCommonslicenseandyourintendeduseisnotpermittedbystatutoryregulationorexceedsthepermitteduse,youwillneedtoobtainpermissiondirectlyfromthecopyrightholder.