Actario: A Framework for Reasoning About Actor Systems

"DUBSJP"'SBNFXPSL GPS3FBTPOJOH"CPVU "DUPS4ZTUFNT 4IPIFJ:BTVUBLF5BLVP8BUBOBCF %FQBSUNFOUPG$PNQVUFS4DJFODF 5PLZP*OTUJUVUFPG5FDIOPMPHZ "(&3&!41-"4)

"CPVU5IJT8PSL #BDLHSPVOE 0WFSWJFXPG"DUBSJP /BNJOHBOE/BNF6OJRVFOFTT $PEF&YUSBDUJPO
'VUVSF8PSLBOE$PODMVTJPO 5BML0VUMJOF w 1SPQPTFTBGSBNFXPSLOBNFE"DUBSJPUIBUJTBJNFEUP GPSNBMJ[FBOEWFSJGZ"DUPSCBTFEBQQMJDBUJPOTPO$PR w *OQBSUJDVMBS JNQMJDJUOBNJOHUFDIOJRVFBOEUIF QSPPGPGOBNFVOJRVFOFTT

#BDLHSPVOE w .FDIBOJ[FEGPSNBMWFSJpDBUJPOPGBDUPSTZTUFNT w .PEFMDIFDLJOH 㾎 %FEVDUJWFBQQSPBDIXJUIQSPPGBTTJTUBOUT w 0QFSBUJPOBMTFNBOUJDTCBTFEPOUSBOTJUJPOT w
/FFEUPQSPWJEFGSFTIOBNFTJOTPNFSVMFT )PXTIPVMEXFUSFBUGSFTIOBNFDSFBUJPO [Watanabe AGERE2013] (NEW) m, q, E[new v], s : A, T m, q, E[m ], s : m , , v, 0 : A, T (s = 0, m fresh)

5IF$PR1SPPG"TTJTUBOU w $PRJTBGPSNBMQSPPGNBOBHFNFOUTZTUFNEFWFMPQFEJO */3*" w $PRBMMPXT w UPEFpOFGVODUJPOTPSQSFEJDBUFT w UPTUBUFNBUIFNBUJDBMUIFPSFNTBOETPGUXBSF
TQFDJpDBUJPOT w UPJOUFSBDUJWFMZEFWFMPQGPSNBMQSPPGTUIFTFUIFPSFNT w UPFYUSBDUDFSUJpFEQSPHSBNTUP0$BNM )BTLFMM PS 4DIFNFCZEFGBVMU

0WFSWJFXPG"DUBSJP w "$PRGSBNFXPSLGPSEFpOJOHBOEWFSJGZJOHBDUPSCBTFE TZTUFNT w "DUBSJPQSPWJEFT w 5ZQFTBOEOPUBUJPOTGPSEFpOJOH"DUPSTZTUFNT w .FDIBOJTNTBOEMFNNBTGPSWFSJGZJOH"DUPSTZTUFNT
OPUZFU w &YUSBDUJPONFDIBOJTNGPS&SMBOH w 4PNFQSPQFSUJFTPGUIFTFNBOUJDTPG"DUBSJPBSF GPSNBMMZQSPWFE FH OBNFVOJRVFOFTT QFSTJTUFODF QSPQFSUZ

8PSLqPXVTJOH"DUBSJP %FTDSJCFBOBDUPSTZTUFN 4QFDJGZBOEWFSJGZEFTJSFEQSPQFSUJFTPGUIFTZTUFN &YUSBDUUIF&SMBOHWFSTJPOPGUIFTZTUFN By User
Actario Framework Types & Notations Impl of an Actor System Spec & Proofs Semantics of the Actor model Veriﬁcation of the Semantics (e.g. name uniqueness) Erlang Code Extractor for Erlang Veriﬁcation Mechanism (Tactics, Lemmas, etc) 1 3 2

&YBNQMF3FDVSTJWF'BDUPSJBM4ZTUFN w DPOUJOVBUJPOQBTTJOHTUZMFGBDUPSJBMTZTUFN fact_behv fact_cont_behv(3, cust) fact_cont_behv(2, c3) factorial_behv(1,
c2) (3, cust) (2, c3) (1, c2) (0, c1) 1 1*1 2*1*1 cust 3*2*1*1 main c1 c2 c3

3FDVSTJWF'BDUPSJBM4ZTUFNJO"DUBSJP w GBDU@DPOU@CFIW w 5IFCFIBWJPSPGDPOUJOVBUJPO BDUPS w .VMUJQMJFTOVNCFSTBOETFOETUIF QSPEVDUUPHJWFODVTUPNFS w
GBDU@CFIW w 5IFCFIBWJPSPGGBDUPSJBMBDUPS UIBUDSFBUFTDPOUJOVBUJPOBDUPST O O ʜ w %FpOFEBT$P'JYQPJOU w CFDBVTFJUJTDBMMFESFDVSTJWFMZ XJUIOPQBSBNFUFST Definition fact_cont_behv (val : nat) (cust : name) := receive (fun msg => match msg with | nat_msg arg => cust ! nat_msg (val * arg); become empty_behv | _ => become empty_behv end). CoFixpoint fact_behv := receive (fun msg => match msg with | tuple_msg (nat_msg 0) (name_msg cust) => cust ! nat_msg 1; become fact_behv | tuple_msg (nat_msg (S n)) (name_msg cust) => cont <- new (fact_cont_behv (S n) cust); me <- self; me ! tuple_msg (nat_msg n) (name_msg cont); become fact_behv | _ => become fact_behv end).

"DUJPOT w "DUJPOTBSFEFpOFEBTUIFDPOTUSVDUPSTPGactions UZQFBOEbehaviorUZQF w actionsBOEbehaviorBSFNVUVBMMZEFpOFEBTDP JOEVDUJWFUZQFTCFDBVTFBCFIBWJPSNBZCFDPNFJUTFMG CoInductive actions
: Type := | new : behavior -> (name -> actions) -> actions | send : name -> message -> actions -> actions | self : (name -> actions) -> actions | become : behavior -> actions with behavior : Type := | receive : (message -> actions) -> behavior. w "DUBSJPIBTDPOWFOJFOUOPUBUJPOTGPSBDUPSQSJNJUJWFTVTJOH OPUBUJPOGFBUVSFPG$PR

0QFSBUJPOBM4FNBOUJDTPG"DUBSJP w "DUBSJPGPSNVMBUFTPQFSBUJPOBMTFNBOUJDTPGUIF "DUPSNPEFMBTMBCFMFEUSBOTJUJPOTZTUFN a ! "hello"; … New
.. a <- new behv; Example: New transition conﬁguration conﬁguration' ... ... ... ... ... ... ... ... a ! "hello"; … .. a <- new behv; New Actor Create (empty) become behv

'PSNBMJ[BUJPOPG'BJSOFTT w (FOFSBMMZ GBJSOFTTJTSFQSFTFOUFEJOVTJOHUIF PQFSBUPSTPGUFNQPSBMMPHJD w 8FFODPEFGBJSOFTTVTJOHUSBOTJUJPOQBUICFDBVTF $PREPFTOPUTVQQPSUUFNQPSBMMPHJD Definition
path := nat -> option config. Definition fairness : Prop := forall (p : path), forall (p’ : path), is_postfix_of p' p -> (forall (l : label), infinitely_often_enabled l p' -> eventually_processed l p').

"DUPS/BNJOH w *OUZQJDBMTFNBOUJDTPGUIF"DUPSNPEFM JUJT BTTVNFEUIBUUIFOBNFPGOFXBDUPSJTGSFTI PS XFNVTUBTTJHOBGSFTIOBNFNBOVBMMZ w *O"DUBSJP UIFTZTUFNBVUPNBUJDBMMZHFOFSBUFB
GSFTIOBNFGPSBOFXMZDSFBUFEBDUPSXIJMF QSFTFSWJOHQSPQFSUJFTPGUIF"DUPSNPEFM w 8FEPO`UOFFEUPNBOVBMMZBTTJHOBGSFTIOBNF w 8FIBWFGPSNBMMZQSPWFEUIBUHFOFSBUFEOBNFT BSFVOJRVF

"DUPS/BNJOH w 5IFOBNFPGBOBDUPSJTSFQSFTFOUFEBTUIFQBJSPG w UIFOBNFPGJUTQBSFOU w UIFOVNCFSPGBDUPSTHFOFSBUFECZUIFQBSFOUTPGBS . .
. ɾA,(A,N) are actor names ɾ(A,N) is the Nth child of A A (A,N) generate A (A,0) (A,1) (A,N) ((A,1),0) ((A,1),1) . . .

1SPPGPG/BNF6OJRVFOFTT w 8FIBWFEFpOFEBOEQSPWFEtrans_invariantUIBUJTB QSFEJDBUFPGBDPOpHVSBUJPOQSFTFSWFECFUXFFOUSBOTJUJPOT w trans_invariantDPOTJTUTPG w chain w gen_fresh 
w no_dup w 5IFQSPPGPGtrans_invariantJTCZJOEVDUJPOPGSFqFYJWF USBOTJUJWFDMPTVSFPGUSBOTJUJPOT

&YUSBDUJPOUP&SMBOH w "DUBSJPQSPWJEFTBDVTUPNDPEFFYUSBDUJPO NFDIBOJTNUBSHFUFEGPS&SMBOH FYUSBDU $PR "DUBSJP &SMBOH behvA()
-> receive Msg -> case Msg of {name_msg, Sender} -> Me = self(), Child = spawn(fun() -> behvB(Me) end), Sender ! {name_msg, Child}, behvA(); _ -> behvA() end end. CoFixpoint behvA := receive (fun msg => match msg with | name_msg sender => me <- self; child <- new (behvB me); sender ! name_msg child; become behvA | _ => become behvA end ).

'VUVSF8PSL w &TUBCMJTIWFSJpDBUJPONFDIBOJTNTUPGBDJMJUBUF EFWFMPQJOHQSPPGT w *OUSPEVDFTVQFSWJTPSNFDIBOJTNMJLF&SMBOHBOE "LLBUPEFTDSJCFGBVMUUPMFSBOU"DUPSTZTUFNT w 1SPPGPGTPVOEOFTTPG&SMBOHFYUSBDUJPO w
/PUDIBOHFUIFTFNBOUJDTPGUIF"DUBSJP QSPHSBNBOEUIFFYUSBDUFE&SMBOHQSPHSBN w 1SBDUJDBMFYBNQMFT

%J⒏DVMUZJO"QQ7FSJpDBUJPO By User Actario Framework Types & Notations Impl of
an Actor System Spec & Proofs Semantics of the Actor model Veriﬁcation of the Semantics (e.g. name uniqueness) Erlang Code Extractor for Erlang Veriﬁcation Mechanism (Tactics, Lemmas, etc) 1 3 2 "CPVUUIJTQBSU w $VSSFOUMZ UPWFSJGZBOBDUPSTZTUFN XFNVTUVTVBMMZ UBLFDBSFPGBMMOPOEFUFSNJOJTUJDDIPJDFTJOUIF DPNQVUBUJPO w 6TFSTNVTULOPXBMMDPOUFOUTPGUIFDPOpHVSBUJPO BDUPSTBOEJUTTUBUF NFTTBHFTJOqJHIU XJUIJUTPSEFS CFGPSFBOEBGUFSBMMUSBOTJUJPOTFWFOJGJUJTOPUSFMBUFE UPUIFQSPPG

4VNNBSZ w 8FQSPQPTF"DUBSJP B$PRGSBNFXPSLGPS EFTDSJCJOHBOEWFSJGZJOHBDUPSCBTFETZTUFNT w /PUBUJPOT w 4FNBOUJDT w
$PEFFYUSBDUJPOGPS&SMBOH w 8FJOUSPEVDFJNQMJDJUOBNJOHUFDIOJRVFBOEIPXUP QSPWFOBNFVOJRVFOFTT

Actario: A Framework for Reasoning About Actor ...

Actario: A Framework for Reasoning About Actor Systems

Shohei Yasutake

More Decks by Shohei Yasutake

Other Decks in Research

Featured

Transcript

"DUBSJP"'SBNFXPSL GPS3FBTPOJOH"CPVU "DUPS4ZTUFNT 4IPIFJ:BTVUBLF5BLVP8BUBOBCF %FQBSUNFOUPG$PNQVUFS4DJFODF 5PLZP*OTUJUVUFPG5FDIOPMPHZ "(&3&!41-"4)

"CPVU5IJT8PSL #BDLHSPVOE 0WFSWJFXPG"DUBSJP /BNJOHBOE/BNF6OJRVFOFTT $PEF&YUSBDUJPO

#BDLHSPVOE w .FDIBOJ[FEGPSNBMWFSJpDBUJPOPGBDUPSTZTUFNT w .PEFMDIFDLJOH 㾎 %FEVDUJWFBQQSPBDIXJUIQSPPGBTTJTUBOUT w 0QFSBUJPOBMTFNBOUJDTCBTFEPOUSBOTJUJPOT w

5IF$PR1SPPG"TTJTUBOU w $PRJTBGPSNBMQSPPGNBOBHFNFOUTZTUFNEFWFMPQFEJO /3" w $PRBMMPXT w UPEFpOFGVODUJPOTPSQSFEJDBUFT w UPTUBUFNBUIFNBUJDBMUIFPSFNTBOETPGUXBSF

0WFSWJFXPG"DUBSJP w "$PRGSBNFXPSLGPSEFpOJOHBOEWFSJGZJOHBDUPSCBTFE TZTUFNT w "DUBSJPQSPWJEFT w 5ZQFTBOEOPUBUJPOTGPSEFpOJOH"DUPSTZTUFNT w .FDIBOJTNTBOEMFNNBTGPSWFSJGZJOH"DUPSTZTUFNT

8PSLqPXVTJOH"DUBSJP %FTDSJCFBOBDUPSTZTUFN 4QFDJGZBOEWFSJGZEFTJSFEQSPQFSUJFTPGUIFTZTUFN &YUSBDUUIF&SMBOHWFSTJPOPGUIFTZTUFN By User

&YBNQMF3FDVSTJWF'BDUPSJBM4ZTUFN w DPOUJOVBUJPOQBTTJOHTUZMFGBDUPSJBMTZTUFN fact_behv fact_cont_behv(3, cust) fact_cont_behv(2, c3) factorial_behv(1,

3FDVSTJWF'BDUPSJBM4ZTUFNJO"DUBSJP w GBDU@DPOU@CFIW w 5IFCFIBWJPSPGDPOUJOVBUJPO BDUPS w .VMUJQMJFTOVNCFSTBOETFOETUIF QSPEVDUUPHJWFODVTUPNFS w

"DUJPOT w "DUJPOTBSFEFpOFEBTUIFDPOTUSVDUPSTPGactions UZQFBOEbehaviorUZQF w actionsBOEbehaviorBSFNVUVBMMZEFpOFEBTDP JOEVDUJWFUZQFTCFDBVTFBCFIBWJPSNBZCFDPNFJUTFMG CoInductive actions

0QFSBUJPOBM4FNBOUJDTPG"DUBSJP w "DUBSJPGPSNVMBUFTPQFSBUJPOBMTFNBOUJDTPGUIF "DUPSNPEFMBTMBCFMFEUSBOTJUJPOTZTUFN a ! "hello"; … New

'PSNBMJ[BUJPOPG'BJSOFTT w (FOFSBMMZ GBJSOFTTJTSFQSFTFOUFEJOVTJOHUIF PQFSBUPSTPGUFNQPSBMMPHJD w 8FFODPEFGBJSOFTTVTJOHUSBOTJUJPOQBUICFDBVTF $PREPFTOPUTVQQPSUUFNQPSBMMPHJD Definition

"DUPS/BNJOH w OUZQJDBMTFNBOUJDTPGUIF"DUPSNPEFM JUJT BTTVNFEUIBUUIFOBNFPGOFXBDUPSJTGSFTI PS XFNVTUBTTJHOBGSFTIOBNFNBOVBMMZ w O"DUBSJP UIFTZTUFNBVUPNBUJDBMMZHFOFSBUFB

"DUPS/BNJOH w 5IFOBNFPGBOBDUPSJTSFQSFTFOUFEBTUIFQBJSPG w UIFOBNFPGJUTQBSFOU w UIFOVNCFSPGBDUPSTHFOFSBUFECZUIFQBSFOUTPGBS . .

"DUPS/BNJOH w 5IFOBNFPGBOBDUPSJTSFQSFTFOUFEBTUIFQBJSPG w UIFOBNFPGJUTQBSFOU w UIFOVNCFSPGBDUPSTHFOFSBUFECZUIFQBSFOUTPGBS . .

"DUPS/BNJOH w 5IFOBNFPGBOBDUPSJTSFQSFTFOUFEBTUIFQBJSPG w UIFOBNFPGJUTQBSFOU w UIFOVNCFSPGBDUPSTHFOFSBUFECZUIFQBSFOUTPGBS . .

1SPPGPG/BNF6OJRVFOFTT w 8FIBWFEFpOFEBOEQSPWFEtrans_invariantUIBUJTB QSFEJDBUFPGBDPOpHVSBUJPOQSFTFSWFECFUXFFOUSBOTJUJPOT w trans_invariantDPOTJTUTPG w chain w gen_fresh

&YUSBDUJPOUP&SMBOH w "DUBSJPQSPWJEFTBDVTUPNDPEFFYUSBDUJPO NFDIBOJTNUBSHFUFEGPS&SMBOH FYUSBDU $PR "DUBSJP &SMBOH behvA()

'VUVSF8PSL w &TUBCMJTIWFSJpDBUJPONFDIBOJTNTUPGBDJMJUBUF EFWFMPQJOHQSPPGT w *OUSPEVDFTVQFSWJTPSNFDIBOJTNMJLF&SMBOHBOE "LLBUPEFTDSJCFGBVMUUPMFSBOU"DUPSTZTUFNT w 1SPPGPGTPVOEOFTTPG&SMBOHFYUSBDUJPO w

%J⒏DVMUZJO"QQ7FSJpDBUJPO By User Actario Framework Types & Notations Impl of

4VNNBSZ w 8FQSPQPTF"DUBSJP B$PRGSBNFXPSLGPS EFTDSJCJOHBOEWFSJGZJOHBDUPSCBTFETZTUFNT w /PUBUJPOT w 4FNBOUJDT w