From Sequential Programs to Multi-Tier Applications by Progr

Modern applications are designed in multiple tiers to separate concerns. Since each tier may run at a separate location, middleware is required to mediate access between tiers. However, introducing this middleware is tiresome and error-prone. We propose a

FromSequentialProgramstoMulti-TierApplications

byProgramTransformation

Institutf¨urInformatik,Universit¨atFreiburg,Germany

MatthiasNeubauerPeterThiemann

{neubauer,thiemann}@informatik.uni-freiburg.de

ABSTRACT

Modernapplicationsaredesignedinmultipletierstosep-arateconcerns.Sinceeachtiermayrunataseparatelo-cation,middlewareisrequiredtomediateaccessbetween

tiers.However,introducingthismiddlewareistiresomeanderror-prone.

Weproposeamulti-tiercalculusandasplittingtransfor-mationtoaddressthisproblem.Themulti-tiercalculusservesasasequentialcoreprogramminglanguageforcon-structingamulti-tierapplication.Theapplicationcanbedevelopedinthesequentialsetting.Splittingextractsoneprocesspertierfromthesequentialprogramsuchthattheirconcurrentexecutionbehavesliketheoriginalprogram.Thesplittingtransformationstartsfromanassignmentofprimitiveoperationstotiers.Aprogramanalysisdeterminescommunicationrequirementsandinsertsremoteprocedurecalls.Thenexttransformationstepperformsresourcepool-ing:itoptimizesthecommunicationbehaviorbytransform-ingsequencesofremoteprocedurecallstoastream-basedprotocol.The naltransformationstepsplitstheresultingprogramintoseparatecommunicatingprocesses.

Themulti-tiercalculusisalsoapplicabletotheconstruc-tionofinteractiveWebapplications.Itfacilitatestheirde-velopmentbyprovidingauniformprogrammingframeworkforclient-sideandserver-sideprogramming.

CategoriesandSubjectDescriptors

D.1.3[PROGRAMMINGTECHNIQUES]:ConcurrentProgramming—DistributedProgramming;

D.1.2[PROGRAMMINGTECHNIQUES]:AutomaticProgramming—ProgramTransformation;F.3.2[LOGICSANDMEANINGSOFPROGRAMS]:SemanticsofProgrammingLanguages—Operationalsemantics

GeneralTerms

Design,Languages,Theory

Permissiontomakedigitalorhardcopiesofallorpartofthisworkforpersonalorclassroomuseisgrantedwithoutfeeprovidedthatcopiesarenotmadeordistributedforpro torcommercialadvantageandthatcopiesbearthisnoticeandthefullcitationonthe rstpage.Tocopyotherwise,torepublish,topostonserversortoredistributetolists,requirespriorspeci cpermissionand/orafee.

POPL’05,January12–14,2005,LongBeach,California,USA.Copyright2005ACM1-58113-830-X/05/0001...$5.00.

Keywords

TypeSystems,Concurrency,ApplicationPartioning

1.INTRODUCTION

Buildingamodernapplicationisnolongerataskofpro-gramminganisolatedmachine.Inmanycases,theapplica-tionhasadistributedmulti-tierarchitecture.Itaccessesdataononeormoredatabaseservers,itsbusinesslogicrunsonanapplicationserver,thepresentationlogicisde-ployedonawebserver,andtheuserinterfacerunsonawebbrowser.Softwareforeachtierisdevelopedseparatelywithapplication-speci ccommunicationinterfacesbetweenthetiers.Thedesignerscreatetheseinterfacesandthepro-grammersimplementthemusingmiddleware.Hence,ontopoftheirusualcodingandtestingactivity,programmersarealsoburdenedwiththequirksofdistribution:testingbecomesmoredi cultand awsinmiddlewarecode—oftencreatedbythird-partyprogrammers—arepotentiallyanad-ditionalsourceoferrorsinthe nalapplication.

Theprogrammer’staskcanbealleviatedbyaprogram-mingframeworkthatautomaticallypreparestheprogramforthephysicaldistribution.Thus,themaindevelopmentactivitytakesplaceinthesimpler,non-distributedsetting.Onlyintegrationtestingandperformancetesting(and,ofcourse, naldeploymentoftheapplication)involvesthedis-tributedproductionsetting.

Thepresentpaperproposessuchaprogrammingframe-workconsistingofacalculus,astaticanalysisthatper-formsanassignmentofcodetolocations,andarangeofprogramtransformationsthatautomaticallyinsertcommu-nicationprimitives,performresourcepooling,and nallysplittheprogramintoseparateprocessestorunatseparatelocations.Locationsinoursenseareusedasanabstractionoverthedi erentphysicalorlogicalplaceswheretiersofthe nalapplicationaresupposedtoreside.

Asastartingpoint,weassumethattheapplicationcon-sistsofsequentialprogramsthatrunconcurrentlyonasin-gleserver.Eachprogramrunsindependentlyonbehalfofaparticularclient.Theprogramsdonotcommunicateexplic-itlyamongthemselvesbuttheyaccessandmodifycommonresourcesontheserver.Thetaskofthetransformationisthustosplitasequentialprogramintopiecesthatruninde-pendentlyfromeachotherondi erenthostsandtoequipthemwithcommunicationprimitivessothatthesequentialsemanticsoftheoriginalprogramispreserved.

Eachoperationusedinthesequentialprogramcarriesanannotationthatindicateswhethertheoperationislocationindependent.Alocationindependentoperationmustnot

Modern applications are designed in multiple tiers to separate concerns. Since each tier may run at a separate location, middleware is required to mediate access between tiers. However, introducing this middleware is tiresome and error-prone. We propose a

havesidee ectsanditmustnotdependondatastoredataparticularlocation.Forexample,anyoperationonaprimi-tivedatatypesislocationindependentwhereasaccessingormodifyingareferenceisnot.Locationdependentoperationscarryalocationannotationthatindicateswheretheoper-ationcansafelytakeplace.Theinterplayofalllocationannotationsdrivesthestaticanalysisoftheprogram.Op-erationsondi erentlocationsmustnotinterferewitheachother.Forexample,databasequeriesmustrunontheappli-cationserverbecausethedatabaseconnectionisareferencethatdoesnotmakesenseoutsideoftheapplicationserver.Incontrast,GUIoperationsrunontheclientbecausetheGUIobjectsarenotpresentontheserver.

Inprinciple,theresultofthethesplittingtransforma-tionisdirectlyapplicabletoannotatedprogramsbutitwouldleadtoprogramssprinkledwithshortcommunica-tions.Sincerepeatedconnectionestablishmentisexpensive,aseparateprogramtransformationperformsresourcepool-ingbyreusingestablishedconnectionsbetweenlocations.Wedescribetheoverallalgorithmabstractlyintermsoftransformationstepsinaprogramcalculus.Thecalculusisbasedonthelambdacalculusequippedwithsynchronouscommunicationprimitives.ItisinspiredbyGayandHole’scalculusofsessiontypes[2].Theircalculusisasimplytypedvariantoftheπ-calculuswithsubtypingandmodelsasyn-chronouscommunicationviaportsandchannels.Channelstransmitheterogeneousdataasprescribedbyasessiontype.UnlikeGayandHole,wehavechosenalambdacalculusbecauseitistrivialtoembedsequentialprogramsinit.Inparticular,ourvariantisbasedonasimply-typed,appliedcall-by-valuelambdacalculusinA-normalform[1].Com-municationinourcalculusisstream-based(portsandchan-nels)withsimilaroperationsasinthecalculusofsessiontypes.A-normalformsimpli esthede nitionofthestaticanddynamicsemanticsandhasbeenusedasanintermedi-atelanguageinseveralcompilers.

Theresultofthetransformationisaprogramwithex-plicitusesoftypedcommunicationprimitivesanalogoustothesocket-basedcommunicationparadigm[15].Animple-mentationwouldmapthecommunicationprimitivestothecommunicationarchitectureprovidedbythechosenmiddle-ware.Alternatively,adirectimplementationintermsofthesocketAPIispossible.

Awebapplicationisaspecialcaseofamulti-tierappli-cationwhereoneormoretiersrunonawebbrowser.Ourframeworkisapplicabletothiscasegivenasuitableme-diatorthatimplementschannelsontopofHTTP.Inthisspecialcase,thesplittingtransformationyieldsaclient-sidesliceandaserver-sidesliceoftheapplication.Theclient’sslicemaybeimplementedbyappletsandtheserver’sslicewithanarbitraryserver-sidescriptingtechnology.

Themaincontributionofthepaperisthepartitioningalgorithm.Itspresentationconsistsofthreesteps:

Wespecifyalocationanalysisthatinfersrequiredcom-municationsbetweenabstractlocations.Theanalysisisstatedintermsofanannotatedsimpletypesystemwithsubtyping.Itisprovedcorrectwithrespecttoalocation-awareoperationalsemanticsusingatype-soundnessargument. Wepresentasuiteoftypedtransformationrulesthatmergeseveralcommunicationsbetweenidenticalpart-nersintolargersectionswithstream-basedcommuni-

letshow_topicrec

letstmt(db,=string_append_4

tid,tpc)=("SELECTletletmsgs="WHERE*tid=’",FROMmessages",tid,"’")in

lethdr=sql_execstring_append(db,stmt)("Topicin",tpc)inletframe_==gui_create_frameshow_rows(db,frame,(hdr)inand

gui_show_frame(frame)msgs)inshow_rowsletb=(db,sql_cursor_has_more_elements

frame,msgs)=

ifb(db,msgs)in

letthen

row=sql_cursor_get_next_row

letcts=sql_cursor_get_column

(db,msgs)in

let(db,row,"contents")in

letlab=gui_create_label(cts)inelse

show_rows_=gui_frame_add(frame,msgs)(frame,lab)inin...

()

Figure1:Originalsequentialprogramcation.Therulesareprovencorrectwithrespecttothelocation-awaresemanticsextendedwithsynchronouscommunication.

Asplittingtransformation nallyextractsconcurrentlyrunningprocessesfromthetransformedexpression.Thistransformationisalsoprovedcorrect.Thetargetcalculusisalanguagewithchannel-basedcommunica-tion.Itstypesystemisanovelvariantofthesystemofsessiontypes[2].Intherestofthepaper,we rstmotivateoursuiteoftransformationswithanexcerptofaclient-serverapplica-tioninSection2.Section3introducesthesourcecalculus,asimply-typed,linearized,call-by-valuelambdacalculus.Section4developstheannotatedtypesystemthatspeci eslocationanalysisforthesourcecalculus.Itformalizesitsstaticanddynamicsemanticsandprovestypesoundness.Section5introducesthemulti-tiercalculuswhichextendsthesourcecalculuswithexplicitchannel-basedcommunica-tionprimitives.Section6de nesthetransformationstepstoimplementconnectionpoolingandSection7presentsthesplittingtransformation.Section8discussesrelatedwork,andSection9concludes.

2.ATINYMULTI-TIERAPPLICATION

Thissectionintroducesanexampleapplication,amessageboard,andshowsanddiscussestheresultsofthelocationanalysisandthesplittingtransformation.Forconcreteness,theexampleisprogrammedinOcaml[9]andiseasytotrans-latetotheformalcalculusintroducedinSection3.

Amessageboardapplicationenablesitsuserstoviewandpostmessagesattachedtocertaintopicsonacentrallyac-cessiblevirtualblackboard.Amessageeitherstartsanewtopicoritrespondstoamessageinanexistingtopic.

Theapplicationdrawsonatleasttwokindsofresourcesthatusuallyresideindi erentphysicallocations:acentraldatabaseserverandawindowingenvironmenthandlinguser

Modern applications are designed in multiple tiers to separate concerns. Since each tier may run at a separate location, middleware is required to mediate access between tiers. However, introducing this middleware is tiresome and error-prone. We propose a

letshow_topicrec

(db[S],tid[S],tpc[S])=letstmt=string_append_4[S]

("SELECT"WHERE*tid=’",FROMmessages",tid,"’")in

letmsgs=sql_exec[S](db,stmt)inlettpc=trans[S->C]tpcinlethdr=string_append[C]("Topic",tpc)inletframe=gui_create_frame[C](hdr)inlet_=show_rows[S,C](db,frame,msgs)inand

gui_display_frame[C](frame)show_rows(db[S],frame[C],msgs[S])=

letb=sql_cursor_has_more_elements[S]

(db,msgs)in

letbb=trans[S->C]ifbinletthen

row=sql_cursor_get_next_row[S]

(db,msgs)in

letcts=sql_cursor_get_column[S]

(db,row,"contents")in

letcts==trans[S->C]letlabgui_create_labelcts

[C](cts)inlet_=gui_frame_add[C](frame,lab)inelse

show_rows[S,C](frame,msgs)in...

()[S,C]

Figure2:Programafterlocationanalysis(fatclient)

interactions.ThedatabaseisaccessibleviaatextualSQLinterfaceandthewindowingenvironmentprovidestheusualGUIwidgets.Thedatabasecontainsonerelationmessageswhereeachtupledescribesonemessage(topic,contents,au-thor,etc).Administrative eldsincludeatopicid(tid)anda agindicatingwhetherthemessagestartsanewtopic.Figure1showstwofunctionstakenfromtheprogram.1Show_topicimplementsabasicoperationofthemessageboard,thedisplayofalistofmessagesforagiventopic.Todoso,it rstqueriesthedatabaseusinganexistingdatabaseconnection,db,foragiventopicid,tid,andpresentsthecontent eldsoftheresultingmessagesetinanewGUIframe.Itreliesonshow_rowstopopulatetheGUIframewithatextlabelforeachmessagewiththattopicid.

ThecodereliesonseverallibraryfunctionstoaccessthedatabaseandtoperformGUIoperations.Inparticular,thefunctionsql_execreturnsacursortotheresultofanSQLquery,thefunctionssql_cursor_...accesstherelationun-derlyingthecursor,andthegui_...functionscreateandmanipulateappropriateGUIwidgets.

Notalllibraryfunctionsarelocationindependent.Thesql_...operationsarenotbecausealltakethedatabaseconnectiondbasaparameter.Theannotation[S]indi-catesthattheconnectionisonlyavailableontheserver,hencethelocationanalysisprescribesthatallsql_...op-erationsmusttakeplaceontheserver,too.Incontrast,theGUIwidgetscanbecreatedanywhere(gui_create_frame,gui_create_label,andgui_frame_add),butthereisalsooneoperation,gui_display_frame,thatmustrunonthe1

hasInOcaml,the_istoawildcardmatchtheleft-handpatternvaluethatofsidetheofaletisapattern,whichmatchesright-handanyside.value.

Thepatternclientmachine(indicatedbythe[C]annotation).Opera-tionslikestring_append_...arelocationindependentandmayexecuteanywhere.

Thelocationanalysisassignstoeachoperationasetoflocationswheretheoperationmusttakeplace.Startingfromtheoperationswitha xedinitialassignment,loca-tioninformationispropagatedthroughtheprogram,B]andan“implicit”communicationy=trans[A->xisinsertedwheneverdataxavailableatAisrequired—butnotyetavailable—atlocationB.Theoutcomeoftheanalysisisdeterminedbyapropagationstrategy.Dependingonthisstrategy,theanalysismayproducefatclientsorthinclientsanditmaychoosetoduplicateoperationsatmultiplelo-cationstoavoidtheoverheadoftransmittingtheirresults.Figure2showsonepossibleoutcomeoftheanalysiswheretheGUIwidgetsareconstructedontheclient.

Atthispoint,theprograminFigure2mayalreadybesplitintoaclientprocessandaserverprocess.However,doingsowouldbeine cientbecauseeachtransbuildsaconnectionbetweenclientandservertotransmitonedataitem.Ourjoiningtransformationaddressesthisine ciency.Itjoinsadjacentcommunications,thusswitchingfromamessage-basedstyletoastream-basedstyle.Themainideaofthejoiningtransformationistointroduceexplicitchannelswithopenandcloseoperationsandthen oatopenoperationstowardscloseoperationsinhopesofmergingthem.Thetransformationhastogointosomecomplicationtodealsmoothlywithconditionalsandwithrecursion.

Finally,thesplittingtransformationextractsfromthean-notatedprogramonesliceforeachlocation.Runningallslicesinparallelisequivalenttorunningtheoriginalpro-gram.Figure3containsthe nalprogramfortheexample.Itcontainstwoprocesseswhichsharethecommunicationportp2.Eachprocesshasthesamestructurebecauseitisessentiallyasliceoftheoriginalprogram.Theserverpro-cess rstopenstheserverendofachannelthroughportpusinglisten.Itssliceofshow_rows rstsendsabooleanindicatingwhetherfurtherdataisfollowing.Ifthatisthecase,itsendsthe rsttupleandattemptstoprocessthenexttuplerecursively.Otherwise,show_rowsexitsandthechannelisclosed.Theclientprocessperformsexactlytheconversecommunications:it rstopenstheclientendofthechannelandthenreceivesdataasitissent.Technically,thecommunicationistypedusingasessiontypeoftheform(µβ.( true→(,β)|false→ε )).Thetypedescribesthepossiblesequencesofcommunicationeventsonachannel: rstreadastring;thenrepeatedlyreadaboolean;theneitherreadatupleandcontinueorclosethechannel.Thelatterchoicedependsonthecommunicationlabelstrueandfalsewhichareusedinthetypeapplica-tionschan{true}andchan{false}.Theyindicateonthetypelevel,whichbranchoftheconditionalistaken.Hence,trueandfalsearenotvalues,butrathercommunicationlabelswhichhaveastatuslikerecordlabels.

Intheexplanationabove,wehaveglossedoverintermedi-atetechnicalstepsthatintroduceadditionalinfrastructureintheterm.Forexample,onestepintroduceschannelswithopenandcloseoperations.Wedefercloserdiscussionoftheintermediatestepstosubsequentsections(Section6and7).

2

ThenewPortexpressionwillbewrittenνpinthecalculus.

Modern applications are designed in multiple tiers to separate concerns. Since each tier may run at a separate location, middleware is required to mediate access between tiers. However, introducing this middleware is tiresome and error-prone. We propose a

letp=newPortin

//serverprocessletrec

show_topic(db,tid,tpc)=letchan=listen(p)inletstmt=string_append_4

("SELECT*FROMmessages","WHEREtid=’",tid,"’")in

letmsgs=sql_exec(db,stmt)inletsendchan(tpc)inlet_=show_rows[chan](db,msgs)inletclose(chan)in()and

show_rows[chan](db,msgs)=

letb=sql_cursor_has_more_elements

(db,msgs)in

letsendchan(b)inifbthen

letchan{true}in

letrow=sql_cursor_get_next_row

(db,msgs)in

letcts=sql_cursor_get_column

(db,row,"contents")in

letsendchan(cts)inshow_rows[chan](db,msgs)else

letchan{false}in()

in...

||

//clientprocessletrec

show_topic()=

letchan=connect(p)inlettpc=recv(chan)inlethdr=string_append("Topic",tpc)inletframe=gui_create_frame(hdr)inlet_=show_rows[chan](frame)inletclose(chan)ingui_display_frame(frame)and

show_rows[chan](frame)=letb=recv(chan)inifbthen

letchan{true}inletcts=recv(chan)in

letlab=gui_create_label(cts)inlet_=gui_frame_add(frame,lab)inshow_rows[chan](frame)else

letchan{false}in()

in...

Figure3:Programsplitupintoseparateprocesses

3.SOURCECALCULUS

Theunderlyingprogrammingmodelisthesimply-typedcall-by-valuelambdacalculuswithintegers,primitiveoper-ations,andrecursion.Tosimplifymatters,thecalculusλAisanintermediatelanguage.Itssyntaxisgivenbyx∈Var,i∈ZExpressions

e::=halt|letdine|ifxtheneelsee|x( x)Statements

d::=x=pfun( x)|x=op( x)|rec{r}r::=ε|x( x)=e|r,rAλAexpressionisasequenceoflet-boundstatements,d,endingeitherinahaltinstruction,aconditional,orajumpwithparameters.Astatementeitherperformsaprimitivefunction,anoperation,orintroducesasetofmutuallyre-cursivejumplabels.

Allargumentsubtermsinexpressionsandstatementsarerestrictedtovariables.Aprimitivefunctionpfun( x)isfreeofsidee ects.Nullaryprimitivefunctionsserveascon-stants.Anoperationop( x)hasunspeci edsidee ects.Ar-gumentsandresultsofprimitivefunctionsandoperationsarerestrictedto rst-ordervalues.Thenotationx standsforthesequencex1,...,xnwherenderivesfromthecontext.Werefrainfromstatingthetypesystemorasemanticsforthesourcecalculusbecausebotharestraightforwardtoderivefromthede nitions(forextendedcalculi)inthesub-sequentsections.

λ Athereisstillonlyoneprogramexecutingwithonecen-tralizedlocusofcontrol.However,ateachlocationonlyasubsetoftheprogram’se ectwillbevisible.Valuesofvariablesareonlyavailableonasubsetoflocations,someoperationsareonlyavailableatspeci clocations,anddatamustbemovedexplicitlyfromonelocationtoanother.Syn-tactically,thereisonenewstatementandonemodi cation:

d::=

···|x=trans[A;B]x|x=opA( x)

4.INTRODUCINGLOCATIONS

AλAexpressiondescribesacomputationatonelocation.

ThissectionextendsλAtoλ A,whichcanexpressthatcer-taincomputationsrunonspeci clocations(i.e.,tiers).In

Thestatementx=trans[A;B]ytransmitsthevalueofy

fromlocationAtolocationB,whereA,B∈N,a nitesetoflocations.ThevalueofymustbeavailableatAbeforeexecutingthestatement.Afterwards,thevalueisavailablethroughxatlocationBaswellasatalllocationsatwhichitwasavailablethroughy.Typically,thetransstatementisusedwithx=ysothatitjustextendstheavailabilityofxtoincludeB.

Onlybasevaluescanbetransmittedbetweenlocations.Functionsandpointers(references)cannotbetransmitted.ThestatementopA( x)performsanoperationthathasasidee ectonlocationAandthusisonlyavailableonthatlocation.Thevaluesofx mustbeavailableatAbeforeexecutingthestatementandtheresultoftheoperationwillbeavailableonlyatAafterwards.Thesidee ectofopA( x)isvisibleonAbutnotonanyotherlocation.

Intherestofthissection,we rstintroducethedynamicsemanticsofλ Aintermsofalabeledtransitionsystem.Next,wepresentatypesystemthattracksthelocationofvaluesinadditiontotheiractualtype.Thetypesystemex-tendsthesystemofsimpletypeswithlocationannotationsandannotationsubtyping.Finally,weprovetypesoundnessforthissystem.

Modern applications are designed in multiple tiers to separate concerns. Since each tier may run at a separate location, middleware is required to mediate access between tiers. However, introducing this middleware is tiresome and error-prone. We propose a

4.1DynamicSemantics

Thedynamicsemanticsofλ Aisde nedbyasmall-step

transitionsystem.Theintermediatestatesofthesystemrequireanextensionofthesyntax,asusual.Therearetwokindsofcomputedvaluesinthesystem:

v

::=

val(i;N)|fun(rec{r};f)

Avaluecanbeeitheraconstantiwithasetoflocations

N,whichindicateswherethevalueisavailable,oritcanbeafunctionconsistingofafunctionnamefandasetrofmutuallyrecursivefunctionde nitions(wherefselectsoneofthefunctionofr).Functionsdonotcarryasetoflocationsbecausetheyareassumedtobeavailableatalllocations.

Theoriginalexpressionsandstatementsareextendedtoadmitvalueswhereverboundoccurrencesofvariablesareallowedintheoriginalsyntax.

Evaluationstepsproducetracesofobservations.Tracesofobservations,w∈l ,arewordsoverobservations,l:

l::=

halt|i0=opA( i)

wherehaltisintendedtoregisterhaltingexpressions,and

i0=opA( i)toregisteraparticularcallpatternofoperationop()executedonlocationA.Withlocs(w),wedenotethesetofalllocations,A,foundalltheobservationsofoperations,i0=opA( i),occurringintheatracew.Throughoutthepaper,wespecifyreductionsasbyatrace, w

familiesofrelationsindexed

.

Figure4de nesseveralnotionsofreductionforλ relatione wA.The

coree

isthecorereductionrelationwhichre-mainsconstantfortherestofthiswork.Itdescribeseval-uationstepsthattransformetoe fect.The w

producingnosideef-t1reductiondealswiththeTransTherelatione w

statement.

ope describesWith w

operationswithsidee ects.

InopA,wedenotereductionsofoperationsonloca-tionA.relations waddition,wwemakewuseofwthefollowingwcombined

w

imp= core∪ op, λ A,pure= core∪ t1, w

w

w

λ

= imp∪ t1.TheA

ruleforprimitivefunctionssubstitutestheresultofthefunctionasdeterminedbyδpfun(apartialfunction)intherestoftheterm.Theresultisavailableatthoseloca-tionswhereallargumentsareavailable.Aprimitiveopera-tiononlyhappensatitsdesignatedlocationandleavesitstrailinthetrace.Operationsbehavenondeterministicallysotheyaremodeledbyarelationδ.Thischoicemayseemoddat rst.However,themodelmustincludethepossibil-itythatoneachlocationfurtherprocessesruninparalleltotheprogram.Thatis,wecannotmodelsidee ectsbypass-ingastateforeachlocationbecausethisstatemaychangebetweentwooperationsofourprogramduetoe ectsfromanotherprocess.Thenondeterministicmodelavoidspass-ingstateexplicitlyandencompassesarbitrarye ectsfromotherprocesses.

Thede nitionofasetofmutuallyrecursivelabelssubsti-tutesafunctionvalueforeachde nedlabel.Thefunctionvalueconsistsofthelabelidenti erpairedwiththede ni-tiongroup.Theconditionaldispatchesevaluationtothetrueorthefalsebranch,asusual.Afunctioncallextractstheselectedfunctionde nitionfromthede nitiongroupandsubstitutestheargumentsintothatfunction’sbody.Sincethefunction’sbodymayrefertootherfunctionsinthede -nitiongroup,itiswrappedinanewletwiththede nitions

τ≤τ

N1 N2N1 N2

τ 2≤τ 1

12 τ 1 →10≤τ 2 →2

Γ ax:τ

Γ ax:τ

τ≤τ aΓax:Γ(x)Figure5:Subtypingandargumentrulesforλ Aofthesamede nitiongroup.

4.2StaticSemantics

Thetypesystemforλ Ahastomodeltwofacetsofeachvalue:itsshapeandthelocationswhereitisavailable.Itkeepstrackoftheshapeusinganunderlyingsimply-typedsystemandaddslocationannotationsande ectstokeeptrackofthelocations.Annotationsubtypingproducespre-ciseanalysisresults[16].

Anannotatedtype,τ,iseitherabasetypebpairedwithasetoflocationsNorafunctiontypewithalocationsetNaslatente ect.ThemeaningofanannotationNisthattheassociateddataitemmustbepresentatalllocationsinN.Thee ectonafunctiontypeindicatesthesetoflocationsthatmayexecuteoperationswhenthefunctionisapplied.

τ::=(b,N)|τ N

→0

N N

Therearethreetypingjudgments.

Γ e!NstatesthateusesvariablesinΓcorrectlyandmayperformoperationsatlocationsN. Γ d Γ !NstatesthatdtransformsΓtoΓ andmayperformoperationsatN. Γ ax:τinfersthetypeforanargumentposition.Subtypinginthesystemisstructuralandinducedsolelybythelocationannotations.Subtyping—asformalizedbythejudgment τ≤τ —expressesthatavaluethatispresentatlocationsetNcansubstituteforavaluethatisonlyex-pectedatasubsetN N.Also,thee ectannotationofasubtypemustbeincludedintheannotationofthesuper-type.Figures5and6containthesubtypingrulesandthetypingrulesforexpressionsandstatements.

Thehaltexpressionhasneitherrequirementsnordoesitperformane ectatanylocation.Thee ectofaletstatementistheunionofthee ectsofthestatementandthebodyexpression.Aconditionalneedsonlybeexecutedonalocationifoneofthebranchescontainscodetobeexecutedonthatlocation.Hence,thevalueoftheconditionneedsonlybeavailableonthelocationsmentionedinthee ectofthebranches.Afunctionapplicationunleashesthelatente ectofthefunction.

Therulesforprimitivefunctionsandoperationsre ecttheiroperationalsemanticsbutusesubtypingtointersectthelocationsetsimplicitly.Arecursivelabelisimplicitlyavailableatalllocations.Thetransstatementcopiesthevalueofy(whichmustbeavailableatlocationA)tolocationBandbindsittoxwithappropriatelychangedtype.

Modern applications are designed in multiple tiers to separate concerns. Since each tier may run at a separate location, middleware is required to mediate access between tiers. However, introducing this middleware is tiresome and error-prone. We propose a

letx=pfun(...val(ij;Nj)...)ine

letrec{fi( xi)=ei}ni=1ineif(val(0;N))thene1elsee2if(val(i;N))thene1elsee2(fun(rec{fi( xi)=ei}nv)i=1;fj))( letx=opA(...val(ij;Nj)...)ineletx=trans[A;B](val(i;N))ine

core

ε

coreε

coreε

coreε

core

i=opA( i)

ε

TT

e[x→val(i;Nj)]ifi=δpfun( i)∧Nj=

nn

e[fj→fun(rec{fi...}i=1;fj)]j=1e2ifN= e1ifi=0andN=

n

letrec{fi( xi)=ei}i=1inej[ xj→v ]e[x→val(i;{A})]e[x→val(i;N∪{B})]

ifi=op( i)∈δ∧A∈

TNj

ε

op

t1ifA∈N

Figure4:Reductionrulesforλ A

Γ e!N

Γ halt!

Γ d Γ !NdΓ e!Ne

deΓ ax:(b,NN1,N2 NΓ

)

e1!N1Γ e2!N2

1212Γ N

ax1: τ →0Γ a x

2:τ 12Γ d Γ !N

( 1≤i≤n)Γ axi:(b,N)

1n( 1≤i≤n)Γ axi:(b,{A})Γ x=op(x1,...,xn) Γ(x:(b,{A}))!{A}

( 1≤j≤n)Γ(fN

i:τ i →i

0)ni=1( xj:τ j) ej!NjΓ rec{fi( xi)=ei}nii=1 Γ(fi:τi →0)ni=1!

Γ ay:(b,N)

A∈NΓ x=transy Γ(x:(b,N∪{B}))!

Figure6:Typingrulesforλ A

4.3Propertiesofλ A

ToconnectλAwithλ Arequiresanerasurefunction|·|mapsanλ

that

AexpressiontoanλAexpressionbyforgettingaboutlocationsandremovingalltrans[A;B]xstatements.Ontypes,theerasurefunctionstripsawayalllocationsetsandalle ects.Erasurehasthefollowingpropertieswithrespecttotheunderlyingunannotatedcalculuswhosetypingjudgmentisindicatedwith 0.Lemma1.

1.IfΓ e !N then|Γ | 0|e |.

2.IfΓ 0ethenthereexistssomeΓ ,e ,andN suchthatΓ e !N and|Γ |=Γande =|e|.Theexpressione pletionsarenotuniquelyde ned,ingeneral.Forexample,considerN={S,C}andoperations

sandcwhichareonlyavailableonSandC,respectively.

source

rstcompletionsecondcompletionx=sS1()x=sS1()

x=sS1()y=x+1x=trans[S;C]xy=x+1

cC(y)y=x+1y=trans[S;C]yhalt

cC(y)cC(y)halt

halt

Therearemanyfurthercompletionsthatperformadditional

uselesstransmissions.Theexamplealsoshowsthatthereisnoobviousnotionofoptimalityorminimalityforcomple-tions.The rstcompletionmayperformfeweroperationsonSwhereasthesecondperformsfeweroperationsonC.ItisnotclearwhichispreferablewithoutmoreinformationaboutCandS.

Forthemoment,weleavethisquestiontoanimplemen-tationoftheanalysisinfuturework.Theimplementationwillmakeitschoicebasedonformalizedpreferencesbetweenlocations.Theimplementationmayevenintroduceredun-dancybyperformingacomputationatmorethanoneloca-tion.Thischoicetradescommunicationwithcomputation.Itisroutinetoprovetypesoundnessforthecalculusλ

A.Thatis,evaluationofatypedclosedexpressioneitherreacheshaltaftera nitenumberofstepsoritkeepsreduc-ingforever.Thetypingrulesforvaluesandtheintermediatestatesarestraightforward.

Lemma2(TypePreservation).Suppose e!N

ande w

λ e then e !N ,N A N,andlocs(w) N.Lemma3(Progress).If e!Nthene=haltor

thereexistse suchthate w

λ Ae andlocs(w) N.Furthermore,wede nethere exivetransitiveclosure w

oftheevaluationrelationasfollows:

ε

e e

e w

e

e

w

e

ew we

Typesoundnessfollowsbystraightforwardinduction.Theorem1.If e!Ntheneithere w

λ Ahaltandlocs(w) Nor,foreache

,ife

w

λ e A

thenthereexistse

suchthate w

λ A

e andlocs(w ) N.

Modern applications are designed in multiple tiers to separate concerns. Since each tier may run at a separate location, middleware is required to mediate access between tiers. However, introducing this middleware is tiresome and error-prone. We propose a

l∈Label,x∈Var,c∈ChannelVarStatements

d::=x=pfun( x)|x=opA( x)|rec{r}

|c=open[A;B]

|c=openP[A;B](p)|close[A;B](c)|x=trans[A;B]c(x)|c{l}r::=ε|x[ c]( x)=e;rExpressions

e::=halt|letdine|ifxtheneelsee

|x[ c]( x)|νp.e

TypesandTypeEnvironments

τ::=(b,N)|[ γ] τ N

→0Γ::= |Γ(x:τ)

SessionTypesandSessionTypeEnvironmentsγ::=ε|(b,γ)|(γ)| li→γi |β|µβ.γΘ::= |Θ(c:ABγ)

Figure7:SyntaxofλMT

5.MULTI-TIERCALCULUS

Themulti-tiercalculus,λMT,isour rstcalculuswithex-plicitcommunicationinstructions.Inthepreviousλ A,thestatementx=trans

[A;B]

calculus,

yjuststatesthenecessityofacommunicationbetweennodesAandBinadeclara-tiveway.Incontrast,λMTaugmentsx=trans[A;B]ywithachannelargumentandprovidesprimitivesthatexplicitlyopenandcloseacommunicationchannel.

Figure7de nesthesyntaxofthemulti-tiercalculusλMT.ThemainextensionofthiscalculuswithrespecttoλAcon-sistsofstatementstoopenachannel(open),totransferdataviaaconnection(trans),andclosetheconnection(close).Incomparisontoλ A,thetransstatementobtainsachannelparameterandfunctionsreceiveadditionalchannelparame-tersc .Achannelvaluecannotbeboundtoanormalvariablebecausethechannelchangesitstypewitheverycommunica-tion.Channelvariablesaretreatedlinearlytosimplifythetrackingofthechangeoftype.

Furtherextensionsareaddedalreadyatthistimesothattheremainingtransformationstepscanallbeexpressedwith-outleavingthecalculusλMT.Aftersplitting,anopenstate-mentyieldstwostatementsthathavetoopenchannelsofmatchingtype.Thecalculushasanexpressionνp.ethatintroducesafreshportnameandanopenPstatementthatopensachannelwithatypeprescribedbytheportp.Open-ingchannelswiththesameportensuresthatthechannels’sessiontypesmatcheveniftheyoccurindi erentplacesintheprogram.Freshnessofportnamesensuresthateachportvalueoccursatmostonceduringtherunofaprogram.Asusual,introductionoffreshnamesiscommutative,thatis,weconsiderexpressionsmodulothesmallestcompatibleequivalencerelation≡containing

νp.e

≡

eifp∈/fv(e)νp.νp.e≡

νp

.νp.e.

Finally,thestatement,c{ },appliesachanneltoastati-callyknownlabel.Likeatypeapplication,ithasnoopera-tionale ect.Intuitively,c{ }selectsoneofseverallabeledtypesforthechannelc:ifchassessiontype →γ, 1→γ1,... ,thenitstypechangestoγafterthechannelappli-cation.Section5.2explainsmoreaboutitsroleintyping.ThetranslationT · fromλ AtoλMTisstraightforward.

Θ,Γ e!N

,Γ halt!

Θ,Γ d Θ ,Γ !NdΘ ,Γ e!Ne

deΓ ax:(b,N)

N1,N2 NΘ,Γ

e1!N1Θ,Γ e2!N21212

Γ N

ax:[ γ] τ →0Γ a z

:τ Θ=( c:γ )

Θ(c:ABγ),Γ e!NΘ,Γ νc.e!NΘ,Γ(p:Portγ) e!N

Figure9:Typingrulesfortarget(λMT)expressionsItreplaceseachoccurrenceofastatement

letx=trans[A;B]yin

byasequenceofstatementsthatopensanexplicitchannelbetweenlocationsAandB,transmitsthecurrentvalueofyfromAtoB,bindsthevaluetox,andclosesbothendsoftheconnection:

letc=open[A;B]in

letx=trans[A;B]c(y)inletclose[A;B](c)in

5.1DynamicSemantics

Thede nitionofthedynamicsemanticsrequirestheex-tensionofthesyntaxwiththesamevaluesasforλ AinSec-tion4.1.Additionally,anewbinderisneededtomodelanopencommunicationchannel.Theexpression

e::=

...|νc[A;B].e

introducesafreshlinearname,c[A;B],forachannelbe-tweenlocationsAandB.

Figure8containsthereductionrules, w

t2,thathandlethenewcommunicationstatements,togetherwithevalu-ationcontexts,E,thatextendthereductionrulesunder

bindingconstructs.

E::=[]|νp.E|νc[A;B].E

Openingachannelintroducesafreshchannelname.The

transmissionofavalueisonlypossiblethroughachannelconnectingtheappropriatelocations.Closingachannelamountstotheremovalofthechannelbinderforc[A;B].Theapplicationofachanneltoalabelhasnooperationale ect.

Forλusethreenotionsw

MT,weistheE-compatibleclosurewofreductions:w MT,pure

E-compatibleclosureof wof w

wcore∪ t2w

, MTisthe

imp∪ t2,and MT()isE-compatibleclosureof wwcore∪ t2Sthe

w

B.B=AopB.

5.2StaticSemantics

ThejudgmentsofthestaticsemanticsofλMTextendthejudgmentsofλ AforexpressionsandstatementsbyanewtypelinearenvironmentΘwhichassociateseachchannel

Modern applications are designed in multiple tiers to separate concerns. Since each tier may run at a separate location, middleware is required to mediate access between tiers. However, introducing this middleware is tiresome and error-prone. We propose a

letc=open[A;B]ineletc=openP[A;B](p)ine1

letx=trans[A;B]c[A;B](val(i;N))ine

νc[A;B].letclose[A;B](c[A;B])ine

letc[A;B]{l}ine

t2ε t2ε t2ε t2ε t2

ε

νc[A;B].e[c→c[A;B]]νc[A;B].e[c→c[A;B]]

e[x→val(i;N∪{B})]ifA∈Nee

Figure8:ReductionrulesforλMT

Θ,Γ d Θ ,Γ !N

( 1≤i≤n)Γ axi:(b,N)

1n Θ,Γ(x:(b,N))!ε

( 1≤i≤n)Γ axi:(b,{A})

1n Θ,Γ(x:(b,{A}))!opA()

( j)( cN

j:Ajγ j),Γ(fi:[ γ]iτ i →i

0)ni=1(

xj:τ j) ej!Njiiiii=1

Θ,Γ(fN

i:[ γ]iτ i →i

0)!ε

Γ ay:(b,N)

A∈NΘ(c:B(b,γ)),Γ x=transc(y) Θ(c:ABγ),Γ(x:τ,N∪{B})!εΓ ay:(b,N)

A∈NΘ(c:A(γ)),Γ x=transc(y) Θ(c:BAγ),Γ(x:τ,N∪{B})!εΘ,Γ c=open[A;B] Θ(c:ABγ),Γ!εΓ(p)=Portγ

Θ,Γ c=openP(p) Θ(c:Bγ),Γ!

Θ(c:ABε),Γ close[A;B]

(c) Θ,Γ!εΘ(c:AB li→γi ),Γ c{lj} Θ(c:ABγj),Γ

Figure10:Typingrulesfortarget(λMT)statements

variabletoitssessiontypeandthepairoflocationscon-nectedbythechannel.

Asessiontype,γ,denotesanω-regularlanguagethatdescribesthesequenceoftypesthattherestoftheses-sioncommunicatesoveronthechannel.Thetypeεindi-catesthatnofurthercommunicationcantakeplaceonachannel,(b,γ)sendsabasevalueandcontinuesaccordingtoγ,and(γ)receivesavalueandcontinues.Thetype l1→γ1,l2→γ2,... isaconditionalsessiontypeguardedbythelabelsl1,l2,...Thechannelapplicationc{li}changesthetypeofctoγi.Eachapplicationoftherecursionoper-atormustbeexpansive,thatis,awell-formedsessiontypedoesnothavesubtermsoftheformµβ1...µβn.β1.Suchsubtermsdonotcorrespondtoregulartrees.Forexample,thetypefromSection2(,µβ.(, true→(β)|false→ε ))denotesthelanguage

{(n|n∈N}∪{(ω}

Sinceeachcommunicationonachannelchangesitssession

type,thevariablesinΘmustobeyalineartypingdiscipline.Figure9containstheannotatedtypingrulesforexpres-sions.Therulesre ectthepreviousrulesetforλ Aandimposeadditionaldemandsontheuseofchannels.Thehaltexpressionrequiresthatallchannelsareclosed.Theconditionalrequiresthatallbranchesmustusethechannelsinthesameway.Theruleforletindicatesthatastate-menttransformsbothenvironments.Afunctioncallpassallchannelstothefunction.

TheannotatedtypingrulesforstatementsappearinFig-ure10.Oftheoriginalrules,onlytheruleforfunctiondef-initionschangessigni cantly.Theadditionalrequirementisthatafunctionmayonlyrefertothechannelspassedasparameters,thatis,afunctiondoesnothavefreechannelvariables.Thetransmissionofavaluechangesthetypeofthechannelasexpected.Closingachannelrequiresthatitssessiontypeisε,whereasopeningachannelinventsasessiontype.Applyingachanneltoalabelselectsthecor-respondingalternativeinthechannel’ssessiontype.

Thesubtypingrulesremainunchanged.Theargumenttypingruleschangeonlymarginally.

5.3ANotionofBisimilarity

Toprovethecorrectnessofthepresentedprogramtrans-formationsweneedtostaterelationshipsbetweensourceprogramsandtheirtransformedcounterparts.Tothisend,weconsidertwoprogramsequivalentiftheperformthesameside-e ectingoperationsinthesameorder.Thisnotionofequivalenceisbestcapturedbyaweakbisimulation[12].Thede nitionofasuitablebisimulationrequiresthatwesplitourtransitionrulesintwoparts:thosereductionsthat

donothaveasidee ect, ww

R1,andthosethatdo, R2.correspondingobservationrelation w

The

→R1,Rtionsusing w2makesw

transi-R1untilwereachatransitionwith R2ingonlythe nalobservationof w

keep-R2.Formally,therelation w

→R1,R2isde nedasfollows:

halt halt→R1,R2

e w

R2e ew

R1e e w

→R1,R2e

e →R1,R2ee →R1,R2eThehaltexpressionisrelatedtoanon-terminatingterm .

Ifwemakeoneobservablestepwith w

R2,thentherelatedexpressionsarealsointheobservationrelation.Unobserv-ablestepsmaybeprependedtotheobservationrelation.FollowingMilner[10]andGordon[3],wede neweakbisimilarityco-inductively—thatis,asgreatest xedpoint—usingthefollowingtwofunctions[ ], thatareparame-

Modern applications are designed in multiple tiers to separate concerns. Since each tier may run at a separate location, middleware is required to mediate access between tiers. However, introducing this middleware is tiresome and error-prone. We propose a

terizedwithrespecttofourtransitionrelations:(Rdef

1,R2,R3,R4)[S]=

{(e,f)|ife w

→R1,R2e

then f withf w

→R3,R4f ande Sf }

(R,R,Rdef

12,R34) S =

(R1,R2,R3,R4)[S]∩(R1,R2,R3,R4)[Sop]op

≈def

R1,R2,R3,R4=gfpS. (R1,R2,R3,R4)[S]

(R1,R2,R3,R4)[S]denotespairsthatreachapairinSbyasimulatedcommonstep,(R1,R2,R3,R4) S isthere-strictionofthesimulationinbothways.Weakbisimilarity,≈R1,R2,R3,R4,isthegreatestrelationwiththeseproperties,i.e.,thegreatest xpointof S .

5.4TechnicalResults

First,typesoundnessisestablishedintheusualwayfromatypepreservationresultandaprogressresult.

Lemma4(TypePreservation).If , e!Nande w

MTe then , e !N withN Nandlocs(w) N.Lemma5(Progress).If , e!Ntheneithere=

haltorthereexistse suchthate w

MTe andlocs(w) N.ThetranslationT de nedatthebeginningofthissec-tionpreservestypingandresultsinprogramswiththesameobservationalbehavior.

Lemma6.IfΓ e!Nthen( Γ ) ,Γ T e !N.

Lemma7.T · ≈

wλ

A,pure

, wop, w w

MT,pure,op6.FROMDATAGRAMSTOSTREAMS

ThetransformationT fromtheprevioussectionworkscorrectly,butitproducesine cientprograms.WheneveravaluefromlocationAisneededatlocationB,theprogramsendsadatagram:itopensachannelfromAtoB,sendsthevalue,andclosesthechannel,again.Theine ciencyliesinthecostofconnectionestablishment.Sincethiscostismuchhigherthanthecostoftransmittingonevalue,itwouldbebetterifthecostforconnectionestablishmentwereamortizedacrossasmanyvaluetransmissionsaspossible.Toavoidrepeatedconnectionestablishment,wede neasetoftransformationrulesonλMTtermsthatseektojoincloseandopenstatementsforachannelwiththegoalofreusingthechannelformultiplecommunications.Es-sentially,thetransformationturnsasequenceofdatagramtransmissionsbetweentwohostsintoastreamconnection.Figure11speci esthetransformationintermsofarela-tion →ES.Thestrategyforapplyingthetransformationrulesisto oateachopenstatementupwardsinalistofstatementsuntiloneofthefollowingholds.

1.Theopenmeetsaclosewithmatching(orreversed)locations.Inthiscase,thetwochannelsarejoinedtogetherandbothstatementsareeliminated.2.Theopenreachesthebeginningofafunctionbody.Ifthefunctionisrecursive,thentheopenissplito inaseparatenon-recursivewrapperfunction.Then,thestandardinliningtransformationcantransporttheopentoallcallsitesofthefunction[14].Thetransfor-mationstopsatfunctionsthatarenotinlineable(e.g.,certaintoplevelfunctions).

3.Theopenreachesthetopofabranchofaconditional.Therearetwopossibilities.Iftheotherbranchhasamatchingopen,thenthetransformationrule rstinsertsachannelapplicationc{l}withlabel tinthetrue-branchand finthefalse-branch.Ifγtandγfaretheoriginaltypesofthechannelsinthetrue-andthefalse-branch,thentheirtypebecomes t→γt, f→γf sothatthechannelscanbejoinedandhoistedinfrontoftheconditional.Ifnomatchingopenisavailableintheotherbranch,thenatransformationrulemayintroduceanewchan-nelbetweenthesourceanddestinationhostthatisopenedandimmediatelyclosed.Thenjoiningtakesplaceasbefore.

Typingispreservedunderthecompatibleclosure ESoftherelation →ES.Thetransformationwith ESleadstoweaklybisimilarprograms.

Lemmasuchthat8.ΘIf ,ΘΓ, Γe !eN!N.ande ESe thenthereexistsΘLemma9. ES

≈

w, wop, wwMT,pureMT,pure, op

7.SPLITTINGTRANSFORMATION

GivenatypederivationforaλMTprogram,thesplittingtransformationextractsforeachlocationaprogramslicesuchthatrunningallslicesinparallelontheirrespectivelocationsisequivalenttorunningtheoriginalprogram.Thetransformationproceedsinthreesteps.The rststepintroducesglobalportnamesforeachconnection.Portnamesserveasgloballyvisiblepointsofcontactbetweentheprocessesgeneratedinstepnumberthree.Thesecondsteppoolstogetherallintroductionsofportnamesatthebeginningoftheprogram.Thethirdstepextractstheslicesfromthetypederivationwhereeachslicecontainsaseparateprocessforeachlocation.

7.1PortIntroduction

The rststepofthesplittingtransformation,theintro-ductionofports,P · ,replaceseachoccurrenceof

letc=open[A;B]in...

byaletexpressionwithopenPheaderthatreferstoanexplicitportnameandissurroundedbyaνabstractionintroducingpreciselythatportname:

νp.(letc=openP[A;B](p)in...)

ThetranslationP preservestyping.Thetranslationproducesweaklybisimilarprograms.

Lemma10.IfΘ,Γ e!NthenΘ,Γ P e !N.

Lemma11.P · ≈

wwwwMT,pure, op, MT,pure, op

7.2PortFloating

Thenextstepmovesallportbinderstothebeginningoftheprogram.Figure12speci esthetransformationintermsofarelation →PB.Thesecondruleliftsaportbinderoutofanarbitraryfunctionde nitionintheblock.

Typingispreservedunderthecompatibleclosure PBoftherelation →PB.Transformingwith PBleadstoweaklybisimilarprograms.

Modern applications are designed in multiple tiers to separate concerns. Since each tier may run at a separate location, middleware is required to mediate access between tiers. However, introducing this middleware is tiresome and error-prone. We propose a

letdinletc=open[A;B]ine →ES

letc=open[B;A]ine →ES

letclose[A;B](c)inletc =open[A;B]ine →ESletrec{f[ c]( x)=letc=open[A;B]ine;

r}ine

→ES

letc=open[A;B]inletdineletc=open[A;B]inee[c →c]

ifx∈var(d)

ifx then(letc=open[A;B]ine1) →ES

else(letc =open[A;B]ine2)

e →ES

letrec{f [ c,c]( x)=e;

f[ c]( x)=letc=open[A;B]inf [ c,c]( x);r}ine

letc=open[A;B]inif t= f

ifxthenletc{ t}ine1

elseletc{ f}ine2[c →c]

letc=open[A;B]inletclose[A;B](c)ine

Figure11:Extendingthescopeofachannel(λMT)

letdinνp.e →PB

letrec{f[ c]( x)=νp.e;r}ine →PB

νp.letdineifp∈var(d)

νp.letrec{f[ c]( x)=e;r}ine

ifp∈var(r)∪{f,x }∪fv(e )

Figure12:Floatingofportbinders

Lemma12.IfΘ,Γ e!Nande PBe thenΘ,Γ

e !N.

Lemma13. PB

w ≈

wwwMT,pure, op, MT,pure, op

kindsofν).

νx.eνx.νy.ee||e

e||(e ||e )(νx.e)||e

≡≡≡≡≡

eifx∈/fv(e)νy.νx.ee ||e

(e||e )||e

νx.(e||e )ifx∈/fv(e ).

7.3

λMTWithoutMagic

Asalastpreparationofthesplittingtransformation,wereplacethemulti-locationcommunicationoperationsinλMTbytraditionalcommunicationoperationsandaddanop-eratorforconcurrentexecution.Forexample,thex=trans[A;B]c(y)statementofλMTspeci essendingofyatlocationAandreceivingofxatlocationB(viachannelc)atthesametime.Also,theopen[A;B]andclose[A;B](c)statementsperformoperationsattwolocations.Hereistheadditionalsyntaxofthe nalcalculusλMTC.

d::=...|closeA(c)|c=listenA(p)|c=connectB(p)

|sendAc(x)|x=recvB(c)e::=...|e||e

Theexpressione1||e2speci estheinterleavedexecutionofe1ande2.Theotherstatementsaretheone-sidedversionsofthepreviouscommunicationstatements.Insteadofanun-speci copenstatementforestablishingachannelbetweentwolocations,therearenowlistenandconnecttocre-ateaserverendandaclientendofachannelforaspeci cport.Inthesamemanner,thereareseparatecommunica-tionoperationstosendanoutboundmessageandtorecvaninboundmessageoveranestablishedchannel.

ThereductionrulesinFig.13workasfollows.Thepair-ingofalistencommandandaconnectcommandforthesameportresultsinachannelabstractionwherethechan-nelnamesarereplacedbythepairednamescandAsend/recvpairforthesamechannelcresultsintransfer-ringthevaluevfromoneendtotheother.Closingbothendsofachannelamountsdroppingthechannelentirely.Theapplicationofachanneltoalabelisasynchronizationconstruct.Itrequiresthesamelabelapplicationattheotherendofthechanneltoproceed.

w

ForλMTC,weuse MTC(,theE-compatibleclosureof

Swww

core∪ t3 B.B=A opB,asthenotionofreduction.

7.5StaticSemantics

7.4DynamicSemantics

Again,theintermediatestatesneedadditionalsyntax:Theνc.eexpressionintroducesapairoffreshlinearnames,cand,thatmodelthetwoendsofachannel.

w

TherearetwonotionsofreductionforλMTC: MTC,pure

www

istheE-compatibleclosureof core∪ t3,and MTCis

ww

theE-compatibleclosureof imp∪ t3(cf.Figure13).Evaluationcontextsarede nedbyE::=[]|E||e|νp.E|νc.E.Bothrelationsconsiderexpressionsmodulothesmall-estcompatibleequivalencerelation≡satisfying(forboth

Figure14containthetypingrulesforthenewstatementsandexpression.Eachportcreatedbyνp.ehasa xedsessiontypeassociatedwithit.Sinceaportisgloballyavailable,itstype,Portγ,doesnotcarryalocationset.Theideaisthatc=listenA(p)bindsctotheserverendofachannelatlo-cationA.Thechannelinheritsitssessiontypeγfromportp.c=connectA(p)createstheclientend.Sincesendingandreceivingofdataisexactlyreversedontheclient,thesessiontypeismirrored—indicatedbyoverlining(cf.Fig-ure15)—beforeitisassignedtothenewclientend.Thesendandrecvoperationspeelo onecommunicationeventfromthechanneltype;sendanoutboundevent,andrecvaninboundevent.Therevisedcloseoperationonlyclosesoneendofachannel.

Theruleforconcurrentexecutionsplitsthelinearchannelenvironmentintotwodisjointparts,oneforeachsubprocess,asindicatedbythe+operator.Thevalueenvironmentis

Modern applications are designed in multiple tiers to separate concerns. Since each tier may run at a separate location, middleware is required to mediate access between tiers. However, introducing this middleware is tiresome and error-prone. We propose a

letc1=listenA(p)ine1||letc2=connectB(p)ine2

letsendAc(v)ine1||letx=recvB()ine2νc.(letcloseA(c)ine1||letcloseB()ine2)

letc{l}ine1||letl}ine2

t3ε t3ε t3ε t3

ε

νc.(e1[c1→c]||e2[c2→e1||e2[x→v]e1||e2e1||e2

Figure13:ReductionrulesforλMTC

Θ,Γ e!N

Θ1,Γ e1!N1Θ2,Γ e2!N2

121212

Θ,Γ d Θ ,Γ !N

Γ(p)=Portγ

Γ(p)=Portγ

Γ ax:(b,N)A∈NΘ(c:(b,γ)),Γ sendc(x) Θ(c:γ),Γ! Θ(c:A(γ)),Γ x=recvA(c) Θ(c:Aγ),Γ(x:b)!

Θ(c:Aε),Γ closeA(c) Θ,Γ!

Figure14:Typingforextendedtargetsyntax,λMTC

li→γi = li→i=ε==β=

=

υ,Figure15:Mirroringofchanneltypes

copiedtobothsubprocessesandtheire ectisgathered.

7.6SliceExtraction

The nalstepstartswithatypederivationfor ,

νp .e!N.ThetransformationTNe

overtheleadingportbinders,extracts νp .e forineachFigureAi16∈NskipsthesliceofoperationsforlocationAi,andputstheminparal-lel.Theresultingprogramhastheformνp .(e 1||...||e m).Strictlyspeaking,thetransformationrequiresatypederiva-tionasinput.Toavoidthisclutter,theinputtermcarriesannotations.Theannotation@Nprovidestheinferredef-fectofanexpressionorstatement.Whenhandlingachan-nel,thetransformationneedstoknowthesourceandtargetlocationsofthechannel.Again,theannotation@{B,C}providesthisinformation.Bothpiecesofinformationarepresentinatypederivation.

Lemma14.Supposethat , νp .e!N.

Then , TNe

Thetransformed νprogramp .e !N.

isweaklybisimilartotheorig-inaloneifweconsidere ectsoneachlocationAseparately.itholdsLemmathat15.TNe

Let · , νp .e!N.ForeachlocationA∈N,

≈ wMT()

, www.opA

, MTC()

,

opA

8.RELATEDWORK

Thesplittingtransformationiscloselyrelatedtoprogram

slicing[17].Recentadvancesinslicingdealwithconcur-rentprograms[11,8],however,whileslicingdoesnotin-troducenewoperations,ourtransformationmapsasequen-tialprogramintoamulti-threadedprogram.Anotherdi er-enceisthatslicingisusuallydrivenbytheprogramdepen-dencygraph,whereasourtransformationisdrivenbyloca-tionanalysiswhichincludesdependencyinformationthroughthetypingrulefortheconditional.

Secureprogrampartitioning(SPP)[19]isacloselyre-latedtransformationthatmapsasequentialprogramtoadistributedprogram.However,thegoalsofSPParequitedi erent.SPPstartsfromaprogramwithcon dentialityandintegrityannotationsforfunctions,data,andanumberofhosts.Fromtheseannotations,SPPpartitionsthepro-gramsuchthateachhostrunsthatpartoftheprogramforwhichitscredentialsareappropriate.Thepartitionfurtherensuresthatthehostonlyreceivesdatauptoitscon den-tialitylevelandthatdatafromthehostisonlytrusteduptoitsintegritylevel.Inanextensionofthatwork[20],theauthorsusereplicationtoincreasethescopeofSPP.

Binding-timeanalysis[7,5]canbeseenasaspecialcaseofthelocationanalysis.Forexample,theTRANSconstructiscloselyrelatedtolifting.However,abinding-timeanaly-sisdistinguishestwomodesofcomputation(staticanddy-namic)whereasalocationanalysisfornlocationsdistin-guishes2ndi erentmodes.

Ourcalculusmaybeviewedasaninstanceofthecapa-bilitycalculus[18]restrictedtosimpletypesandspecializedtoparticularresources(channelsandlocations).Thisspe-cializationenablesustoexploitpropertiesbeyondthereachofthecapabilitycalculus.

Sessiontypes[2]haveemergedasanexpressivetypingdis-ciplineforheterogeneous,bidirectionalcommunicationchan-nels.Eachmessagemayhaveadi erenttypewiththepos-siblesequencesofmessagesdeterminedbythechannel’sses-siontype.Suchatypedisciplinesubsumestypingsfordata-gramcommunicationaswellasforhomogeneouschannels.Researchontheparallelimplementationoffunctionallan-guagesisconcernedwiththeautomaticdetectionofimplicitparallelismandthespeculativeevaluationofexpressions,e.g.,[13,4].Ouranalysisdoesnotdetectparallelismbutde-terminesindependentslicesofprogramswithexplicitcom-municationinterfaces.Thereisnospeculativeevaluationinourtransformedprograms,althoughthesplittingtrans-formation(guidedbythelocationanalysis)mayintroduceredundancybyperforminglocationindependentoperationsinmorethanonelocationsimultaneously.

9.CONCLUSIONSANDFUTUREWORK

Wehavepresentedalocationanalysisthatenablessplit-tingofanapplicationintoslicesthatexecuteindependently

Modern applications are designed in multiple tiers to separate concerns. Since each tier may run at a separate location, middleware is required to mediate access between tiers. However, introducing this middleware is tiresome and error-prone. We propose a

ToplevelTNeExpressionsT{eA νp.e =νp.Expressionse TNe=T Aee1 e ||...||TAe1,...,Am} m e ife≡νp.e TAeTAe TAe

halt letd =inhalte =letde=

ifx thenTAe d inTA e ifxe1else2@N thenTAe

halt e1 elseTAe

e2 Aotherwise

∈N

TAe

=

x[ c] ( z()@x)N[T Athalt c ]TAt

z Aotherwise

∈N

StatementsTAd =

x=

pfunx=( xpfun)@N( x)A∈N

rec{}otherwiseT

Ad

x=opA=

( x)

x=opA

( x)A=A

TAd rec{}s=[B;C]

8

openP

(p)

otherwiseB=A=<c=listenA(p):

c=connectA

(p)C=A

rec{}TA

d

close[B;C](c) otherwise=

closeA(c)A=B∨A=C

rec{}otherwise

TAd

=recrec{fi[ ci]( xi)=e{fi[TAt

i}ni=1tTAd

c i ](TA x

i )=TAe ei }ni=1trans[B;C]8

c(x)

A=

<sendc(x)

=B:x=recv(c)A=Crec{}

TAd

c{lj=

}BC otherwisec{lj}A=B∨A=C

rec{}otherwise

ParameterlistsTAtT =() TAt

x,x@N =At

TAt

x x

,xAotherwise∈NFigure16:SliceextractioninλMTC

inparallelandthatcommunicateviatypedstreams.The

analysisandtheaccompanyingtransformationsenablethedevelopmentofdistributedapplicationsinalocalsetting.Eachofthetransformationstepsisprovencorrect.

Ongoingworkconsidersthee cientimplementationofthelocationanalysis.Thechallengeisthattheanalysismustbecon gurablewithrespecttolocationpreferencesandcommunicationrequirements.Thepresentworkonlygivesaspeci cation.Practicalexperiencewillshowifapolymorphicanalysisisrequired.

Ingeneral,themappingtotierswillbeamulti-languageissuethatrequiresanadditionaltranslationstepfromtheframework’slanguagetothedesiredtargetlanguages.Al-ternatively,aheterogenousframeworkmightbeconsideredwhereeithertheanalysisappliesdirectlytodi erentlan-guages.

Acknowledgment

Weareindebtedtotheanonymousreviewerswhosenumer-ousandextensivecommentshelpedtoimprovethepresen-tationsigni cantly.

10.REFERENCES

[1]C.Flanagan,A.Sabry,B.F.Duba,andM.Felleisen.The

essenceofcompilingwithcontinuations.InProceedingsofthe1993ConferenceonProgrammingLanguageDesignandImplementation,pages237–247,Albuquerque,NewMexico,June1993.

[2]S.GayandM.Hole.Typesandsubtypesforclient-server

interactions.InD.Swierstra,editor,Proceedingsofthe1999EuropeanSymposiumonProgramming,number1576in

LectureNotesinComputerScience,pages74–90,Amsterdam,TheNetherlands,Apr.1999.Springer-Verlag.

[3]A.Gordon.Bisimilarityasatheoryoffunctionalprogramming.

TheoreticalComputerScience,228(1-2):5–47,Oct.1999.

[4]J.GreinerandG.E.Blelloch.Aprovablytime-e cientparallel

implementationoffullspeculation.ACMTransactionsonProgrammingLanguagesandSystems,21(2):240–285,1999.[5]F.Henglein.E cienttypeinferenceforhigher-order

binding-timeanalysis.InHughes[6],pages448–472.

[6]J.Hughes,editor.FunctionalProgrammingLanguagesand

ComputerArchitecture,number523inLectureNotesinComputerScience,Cambridge,MA,1991.Springer-Verlag.[7]N.Jones,C.Gomard,andP.Sestoft.PartialEvaluationand

AutomaticProgramGeneration.Prentice-Hall,1993.

[8]J.Krinke.Context-sensitiveslicingofconcurrentprograms.In

Proceedings9thEuropeanSoftwareEngineeringConference,pages178–187.ACMPress,2003.

[9]X.Leroy.TheObjectiveCamlsystemrelease3.02,

Documentationanduser’smanual.INRIA,France,July2001.http://pauillac.inria.fr/caml.

[10]municationandConcurrency.PrenticeHall,

EnglewoodCli s,NJ,1989.

[11]M.G.NandaandS.Ramesh.Slicingconcurrentprograms.In

ProceedingsoftheInternationalSymposiumonSoftwareTestingandAnalysis,pages180–190.ACMPress,2000.

[12]D.Park.Concurrencyandautomataonin nitesequences.In

Proceedingsofthe5thGI-ConferenceonTheoretical

ComputerScience,number104inLectureNotesinComputerScience,pages167–1183.Springer-Verlag,1981.

[13]S.L.PeytonJones.Parallelimplementationsoffunctional

programminglanguages.TheComputerJournal,32(2):175–186,1989.

[14]unchbury.Unboxedvaluesas rst

classcitizensinanon-strictfunctionallanguage.InHughes[6],pages636–666.

[15]W.R.Stevens.UNIXNetworkProgramming.PrenticeHall

SoftwareSeries,1990.

[16]Y.M.TangandP.Jouvelot.E ectsystemswithsubtyping.In

W.Scherlis,editor,Proc.ACMSIGPLANSymposiumonPartialEvaluationandSemantics-BasedProgram

ManipulationPEPM’95,pages45–53,LaJolla,CA,USA,June1995.ACMPress.

[17]F.Tip.Asurveyofprogramslicingtechniques.J.

ProgrammingLanguages,3(3):121–189,1995.

[18]D.Walker,C.Crary,andG.Morrisett.Typedmemory

managementviastaticcapabilities.ACMTransactionsonProgrammingLanguagesandSystems,22(4):701–771,July2000.

[19]S.Zdancewic,L.Zheng,N.Nystrom,andA.C.Myers.Secure

programpartitioning.ACMTransactionsonComputerSystems,20(3):283–328,2002.

[20]L.Zheng,S.Chong,A.C.Myers,ing

replicationandpartitioningtobuildsecuredistributedsystems.InProceedingsofthe2003IEEESymposiumon

SecurityandPrivacy,page236.IEEEComputerSociety,2003.

本文来源：https://www.bwwdw.com/article/y6vq.html