王俊吉-RustConf2023-RustBelt.pptx

1、第三屆中國第三屆中國Rust開發者大會開發者大會王俊吉RustBelt-Rust的形式化語義模型的形式化語義模型OutlineBackground RustBelt Project Rust Types OverviewRust SemanticsType SystemThe own PredictExclusive Ownership&Mutable BorrowExamplesRcLogics Hoare Logic Separation LogicBackgroundERC Project RustBelt2015-2021Unlike C/C+,Rust is a safe langu

2、ageBut,like C/C+,Rust is also an unsafe languageThere are guaranteed memory safety,thread safety,.There are plenty of unsafe codes in Rusts standard library.use after freedata racearray-index overflowuse after freedata racearray-index overflow?.RustBelt ProjectBackgroundRalf Jung,et.al.RustBelt:Secu

3、ring the Foundations of the Rust Programming Language.In POPL 2018:ACM SIGPLAN Symposium on Principles of Programming LanguagesRalf Jung.Understanding and Evolving the Rust Programming Language.PhD dissertation,Saarland University,August 2020Recipient of the 2020 ACM Doctoral Dissertation Award Hono

4、rable MentionRecipient of the 2021 ACM SIGPLAN John C.Reynolds Doctoral Dissertation AwardRecipient of the 2021 ETAPS Doctoral Dissertation AwardRecipient of the 2021 Otto Hahn MedalRalf JungAssistant professor,Institute for Programming Languages and Systems,ETH ZrichRustBelt ProjectBackgroundIris:A

5、 Higher-Order Concurrent Separation Logic FrameworkRustBelt:Securing the Foundations of the Rust Programming LanguageCoq Proof Assistant:A Formal Proof Management Systembuilt on top ofbuilt on top ofRust Types OverviewBackgroundT&mut mut T&Tmutable borrowimmutable borrowcoercionmovemutablereborrowre

6、borrow()dropnewexclusivesharedownsborrowsHoare LogicLogicsCPreconditionPostconditionProgramGiven the precondition“P”,if we execute the program“C”and it terminates,it will hold the postcondition“Q”.PQLogicsTrue let x=10 x=10 x=3 x+=1 x=4True loop FalseHoare LogicLogicsP:x vOwnershipWe own“x”,and“x”po

7、ints to“v”.DisjointnessGiven“(x v)(y w)”,we know that“x y”,i.e.,they do not alias.P Q Separation Logic(Iris)PQvxyP Q Magic wandConsuming resource“P”,we can reach resource“Q”.QPwhat we acually ownLogics(x v)(x w)False(x v)(x w)v=wSeparation Logic(Iris)(x=1)(y=2)(x=1)(y=2)Resources,uniqueResources,not

8、 duplicableNon-resourcesLogicsTrue let x=Box:new(1)x 1(x 1)(y 1)*x+=*y (x 2)(y 1)x drop(x)TrueSeparation Logic(Iris)Type System of Rust(selective)Rust SemanticsRust TypeRust Typeboolbool|intintboolbool|BigIntBox&a mut mut T|&a T(T1,T2)|()enum enum Type A(T1),B(T2)|enumenum Type or !|OptionAbstract m

9、achine!The own own PredictRust Semantics boolbool.own(v):=v =truetrue v =falsefalse .own(v)-A relation between a type and a list of values:=.own(v).own(v).own(v):CopyList concatentation intint.own(v)1 2.own(v):=z .v =z:=v1,v2.(v =v1+v2)1.own(v1)2.own(v2)Exclusive Ownership&Mutable BorrowsRust Semant

10、icsIt owns a location value“”;(under full borrow of lifetime“”)In Rust,T,Box can be borrowed as&a mutmut T ownown .own(v)“”points to a value of type“”;We can deallocate“”;It owns a location value“”;“”points to a value of type“”;.own .ownRc(simplified model,without weak references)ExamplesIt owns a l

11、ocation value“”;rcrc .own(v)“”points to a tuple of a counter“c”and data“w”cntdataRcAnother RcHowever,multiple Rcs can point to the same value,which breaks the uniqueness of“”.Rc:The shared_ownshared_own PredictExamples“shared_own”ties up the counter“c”and the proportion“q”of the partial tdataRcRc ca

12、n be cloned,with its cnt increased 1.Cloned Rccnt+1data rcrc .own(v)When Rc:cnt is 1,it owns the dataRc:cloneExamples rcrc .own(x)let y=x.clone()rcrc .own(x)rc rc .own(y)t+=1;let y=ptr:read(x)GoalProofsketchRc:cloneExamplesGoalRc:cloneExamplesGoalRc:cloneExamplesGoalProofsketch rcrc .own(x)rcrc .own(y)Q.E.D.let y=ptr:read(x)Thank you！