Upgrade to Pro — share decks privately, control downloads, hide ads and more …

Actario: A Framework for Reasoning About Actor ...

Actario: A Framework for Reasoning About Actor Systems

Shohei Yasutake

October 26, 2015
Tweet

More Decks by Shohei Yasutake

Other Decks in Research

Transcript

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

    'VUVSF8PSLBOE$PODMVTJPO  5BML0VUMJOF w 1SPQPTFTBGSBNFXPSLOBNFE"DUBSJPUIBUJTBJNFEUP GPSNBMJ[FBOEWFSJGZ"DUPSCBTFEBQQMJDBUJPOTPO$PR w *OQBSUJDVMBS JNQMJDJUOBNJOHUFDIOJRVFBOEUIF QSPPGPGOBNFVOJRVFOFTT
  2. #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)
  3. 5IF$PR1SPPG"TTJTUBOU w $PRJTBGPSNBMQSPPGNBOBHFNFOUTZTUFNEFWFMPQFEJO */3*" w $PRBMMPXT w UPEFpOFGVODUJPOTPSQSFEJDBUFT w UPTUBUFNBUIFNBUJDBMUIFPSFNTBOETPGUXBSF

    TQFDJpDBUJPOT w UPJOUFSBDUJWFMZEFWFMPQGPSNBMQSPPGTUIFTFUIFPSFNT w UPFYUSBDUDFSUJpFEQSPHSBNTUP0$BNM )BTLFMM PS 4DIFNFCZEFGBVMU 
  4. 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 
  5. 8PSLqPXVTJOH"DUBSJP  %FTDSJCFBOBDUPSTZTUFN  4QFDJGZBOEWFSJGZEFTJSFEQSPQFSUJFTPGUIFTZTUFN  &YUSBDUUIF&SMBOHWFSTJPOPGUIFTZTUFN  By User

    Actario Framework Types & Notations Impl of an Actor System Spec & Proofs Semantics of the Actor model Verification of the Semantics (e.g. name uniqueness) Erlang Code Extractor for Erlang Verification Mechanism (Tactics, Lemmas, etc) 1 3 2
  6. 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).
  7. "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
  8. 0QFSBUJPOBM4FNBOUJDTPG"DUBSJP w "DUBSJPGPSNVMBUFTPQFSBUJPOBMTFNBOUJDTPGUIF "DUPSNPEFMBTMBCFMFEUSBOTJUJPOTZTUFN  a ! "hello"; … New

    .. a <- new behv; Example: New transition configuration configuration' ... ... ... ... ... ... ... ... a ! "hello"; … .. a <- new behv; New Actor Create (empty) become behv
  9. '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').
  10. "DUPS/BNJOH w *OUZQJDBMTFNBOUJDTPGUIF"DUPSNPEFM JUJT BTTVNFEUIBUUIFOBNFPGOFXBDUPSJTGSFTI PS XFNVTUBTTJHOBGSFTIOBNFNBOVBMMZ w *O"DUBSJP UIFTZTUFNBVUPNBUJDBMMZHFOFSBUFB

    GSFTIOBNFGPSBOFXMZDSFBUFEBDUPSXIJMF QSFTFSWJOHQSPQFSUJFTPGUIF"DUPSNPEFM w 8FEPO`UOFFEUPNBOVBMMZBTTJHOBGSFTIOBNF w 8FIBWFGPSNBMMZQSPWFEUIBUHFOFSBUFEOBNFT BSFVOJRVF 
  11. "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) . . .
  12. "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) . . .
  13. "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) . . .
  14. &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 ).
  15. %J⒏DVMUZJO"QQ7FSJpDBUJPO By User Actario Framework Types & Notations Impl of

    an Actor System Spec & Proofs Semantics of the Actor model Verification of the Semantics (e.g. name uniqueness) Erlang Code Extractor for Erlang Verification Mechanism (Tactics, Lemmas, etc) 1 3 2  "CPVUUIJTQBSU w $VSSFOUMZ UPWFSJGZBOBDUPSTZTUFN XFNVTUVTVBMMZ UBLFDBSFPGBMMOPOEFUFSNJOJTUJDDIPJDFTJOUIF DPNQVUBUJPO w 6TFSTNVTULOPXBMMDPOUFOUTPGUIFDPOpHVSBUJPO BDUPSTBOEJUTTUBUF NFTTBHFTJOqJHIU XJUIJUTPSEFS  CFGPSFBOEBGUFSBMMUSBOTJUJPOTFWFOJGJUJTOPUSFMBUFE UPUIFQSPPG
  16. 4VNNBSZ w 8FQSPQPTF"DUBSJP B$PRGSBNFXPSLGPS EFTDSJCJOHBOEWFSJGZJOHBDUPSCBTFETZTUFNT w /PUBUJPOT w 4FNBOUJDT w

    $PEFFYUSBDUJPOGPS&SMBOH w 8FJOUSPEVDFJNQMJDJUOBNJOHUFDIOJRVFBOEIPXUP QSPWFOBNFVOJRVFOFTT