outline-basicstudiesincomputingscience

1、Xiaoju Dong(董笑菊)Joint course with Prof. Yuxi Fu(傅育熙)BASICS, Shanghai Jiao Tong Universityxjdong@sjtu.edu.cnhttp://basics.sjtu.edu.cn/~xiaoju/concur17,Concurrency Theory,問題1,公安機關正在調查一宗盜竊案，現(xiàn)獲得事實如下： A或B盜竊了文物若A盜竊了文物，則

2、作案時間不可能在午夜前若B證詞正確，則在午夜前屋里燈光未滅若B證詞不正確，則作案時間發(fā)生在午夜前午夜時屋里燈光滅了試問誰是盜竊犯？,2024年3月17日星期日,BASICS,2,問題1,公安機關正在調查一宗盜竊案，現(xiàn)獲得事實如下： A或B盜竊了文物若A盜竊了文物，則作案時間不可能在午夜前若B證詞正確，則在午夜前屋里燈光未滅若B證詞不正確，則作案時間發(fā)生在午夜前午夜時屋里燈光滅了試問誰是盜竊犯？,2024年3月17日星

3、期日,BASICS,3,命題邏輯,問題2,電燈開關兩個開關A、B同時控制一盞燈C,只要有一個開關處于開啟狀態(tài)燈就會亮只有兩個開關之一處于開啟狀態(tài)燈才亮請具體列出燈C在開關A和B處于什么情況下會亮,問題2,電燈開關兩個開關A、B同時控制一盞燈C,只要有一個開關處于開啟狀態(tài)燈就會亮只有兩個開關之一處于開啟狀態(tài)燈才亮請具體列出燈C在開關A和B處于什么情況下會亮,數(shù)字邏輯,Formal Methods,In comput

4、er science, specifically software engineering and hardware engineering, formal methods are a particular kind of mathematically based techniques for the specification, development and verification of software and hardware

5、 systemsThe use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliabilit

6、y and robustness of a design.,2024年3月17日星期日,BASICS,6,Formal Methods,Formal methods are best described as the application of a fairly broad variety of theoretical computer science fundamentals, in particular logic calculi

7、, formal languages, automata theory, discrete event dynamic system and program semantics, but also type systems and algebraic data types to problems in software and hardware specification and verification,2024年3月17日星期日,B

8、ASICS,7,Xiaoju Dong(董笑菊)Joint course with Prof. Yuxi Fu(傅育熙)BASICS, Shanghai Jiao Tong Universityxjdong@sjtu.edu.cnhttp://basics.sjtu.edu.cn/~xiaoju/concur17,Concurrency Theory,9,Concurrency,In computer science, con

9、currency is a property of systems several computations are executing simultaneouslyand potentially interacting with each other,10,Concurrency,Computation any type of calculationuse of computer technology in Informati

10、on processing (e.g. query in a database)(electronic)computers, quantum computers, DNA computers, molecular computers, etc.a process following a well-defined model expressed in an algorithm, protocol, etc.,11,Concurrenc

11、y,Interaction (or communication)Hand-shaking (synchronization)Value-passingName-passingProcess-passing……,12,Concurrency,An example – sorting,,,,,,sequential,concurrent,,,,,concurrent (with interaction),13,Concurrenc

12、y,An example – sortingMore examples ?,14,Concurrency,An example – sortingMore examples ?reading & eating an applechatting & downloadingCS web servicecells in our body……,15,Concurrency theory,An active fie

13、ld of research in theoretical computer scienceFormalisms for modeling and reasoning about concurrencyOne of the first proposals: Carl Adam Petri, Petri Nets, in the early 1960s,Complex concurrent systems,Shared resou

14、rces(1) x := 1 Sequential: determinedConcurrency: non-determined,(2) x := 0 x := x+1,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,17,Content,Process calculiCalculus of Communicating Systems (CCS)Name Passing Calc

15、ulus (Pi calculus)Petri nets,References,CCSCommunication and Concurrency.Robin Milner. Prentice Hall, 1989. Pi calculusCommunicating and Mobile Systems: The π-calculus. Robin Milner. Cambridge University Press, 199

16、9. The π-calculus: A Theory of Mobile Processes. Davide Sangiorgi. Cambridge University Press, 2001. Petri netsPetri nets – an introduction ,Wolfgang Reisig, Springer-Verlag, 1982,,,,Review,2024年3月17日星期日,上海交通大學計算

17、機系BASICS實驗室,20,Sequential Computation,The Concept of ComputationSequential Computationa linearly ordered sequence of atomic actions,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,21,Some Models,Theory of Sequential ComputationTuri

18、ng machine (Turing)Computation as mechanical operation?-Calculus (Church)Computation as ?-reductionRecursion theory (Kleene etc.) Computation as function compositionComputation denotes function,2024年3月17日星期日,上海交通大學

19、計算機系BASICS實驗室,22,Turing Machine,A Turing machine is a theoretical device that manipulates symbols on a strip of tape according to a table of rulestape head transition function (a table of instructions, an action tabl

20、e)state registerReferenceElements of the theory of computation, Harry LewisIntroduction to Theory of Computation, Michael Sipser,Turing Machine,2024年3月17日星期日,BASICS,23,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,24,?-Calculus,

21、Computation as Term RewritingTermt := x variable tt’ application ?x.t abstractionReduction(?x.t)s ? t{s/x}Examples: (?x.xx) (?x.xx) ? (?x.xx) (?x.xx)u((?x.t)s) ? u(t{s/x})

22、 (?x.f(xx)) (?x.f(xx)) ? f((?x.f(xx)) (?x.f(xx))),Fixed Point Theorem,For all lambda expressions F there exists X such that FX=X.Proof. Suppose W ≡ ?x.F(xx) and X≡WW. X ≡ WW ≡ (?x.F(xx))W = F(WW) ≡ FX.,2024年3月17日星期日,上海

23、交通大學計算機系BASICS實驗室,26,Recursive Function,Computable Functions as Recursive FunctionsBasic IdeaSome initial functionsSome rules to compose new functionsCompositionRecursionMinimalization,Recursive Function,The Zero f

24、unctionf(x) = 0The Successor functionf(x) = x+1The Projection functionf(x1, …, xn, i) = xiSubstitution/compositionf(y1, …, yn)=f(g(x1), …, g(xn)), where yi=g(xi),2024年3月17日星期日,BASICS,27,Recursive Function,Recu

25、rsionh(x, 0) = f(x); h(x, y+1) = g(x, y, h(x, y)) e.g. x+y: x+0=x; x+(y+1)=(x+y)+1Minimization,2024年3月17日星期日,BASICS,28,Ackermann Function,2024年3月17日星期日,BASICS,29,The Ackermann function is not primitive recursive.

26、It grows faster than all the primitive recursive functions.,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,30,Church Turing Thesis,FactEquivalence in terms of expressive powerChurch Turing ThesisThe computable functions are preci

27、sely the recursive functionsLogical foundation of computationComputation as logical object,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,31,Concurrent System,All Systems are Concurrent SystemsConcurrency is an Intrinsic Property

28、Concurrency is a Property Rather Than a Definition,EXAMPLES,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,33,Example I: Ether Net,,,,Medium,Sender,Receiver,,,Is the Capacity of Medium Unbounded?Is the Order of the Message Respected

29、?,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,34,Example II: Vending Machine,Vending MachineThe slot can accept 1c coinThe buttons can be pressed for a cup of tea or coffeeTea or coffee can be collected from the trayInteractio

30、n between Machine and Buyer,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,35,Transition,The State TransitionBlue is the initial stateGreen is the state after receiving 1cOne of the other two states is reached after the tea-button

31、 or the coffee-button is pressed,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,36,Nondeterminism,The Vending Machine Out of OrderHaving taking in 1c, the vending machine disable the tea-button or coffee-button nondeterministically,

32、2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,37,Equivalence,Are The Two Systems Equivalent?They are equivalent as automataAs concurrent systems they are not equivalent, because the ways buyers interact with them are differentObs

33、ervational Equivalence,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,38,Example III: Concurrent Program,Sequential ProgramsX:=2X:=1; X:=X+1Both Programs Assigns 2 to XTwo Programs are Equivalent,Concurrent ProgramsX:=2 | X:=2(

34、X:=1; X:=X+1) | X:=2The Results are NondeterministicTwo Programs are not EquivalentInterleaving semantics,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,39,Example IV: A Unit Transmitter,The transmitter receives a message through

35、inIt sends out a message through outRepeat,,,,C,in,out,,,,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,40,Connecting Unit Transmitter,,,,C,in,out,,,,,,,C,C,.....,How does it behave?,???????????????,n-times,2024年3月17日星期日,上海交通大學計算機

36、系BASICS實驗室,41,Example V: Transmitter with Acknowledgment,The transmitter receives a message through inIt sends out a message through outIt receives acknowledgment through ackoutIt sends acknowledgment through ackinRe

37、peat,,,,D,in,out,,,,,,,ackout,ackin,,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,42,Example V: Transmitter with Acknowledgment,,,,D,in,out,,,,,,,ackout,ackin,,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,43,Chaining Acknowledgment,,,D,in,out

38、,,,,,,,D,D,.....,ackout,,,,ackin,,???????????????,n-copies,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,44,Chaining Acknowledgment,,,D,in,out,,,,,,,D,D,.....,ackout,,,,ackin,,???????????????,n-copies,How does it behave?,2024年3月17日星

39、期日,上海交通大學計算機系BASICS實驗室,45,Concurrent Computation,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,46,Models of Concurrent Computing,Petri Net (Petri;1962)Information flow in concurrent systemsProcess Algebra (Bergstra;1970’s)Purely

40、algebraic approachProcess Calculus (Milner, Hoare;1970)Operational approachSubject to studies of combined approach,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,47,Concurrency Theory,Studies on Semantic Models forDistributed com

41、putingConcurrent ComputingMobile computing (mobile computation)Grid ComputingGlobal ComputingInternet ComputingCasts Light on Our Computing Practice,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,48,Concurrency Kaleidoscope,Too

42、 Rich to be Understood at the MomentToo Rich to be Captured by one FormalismMany Complimentary Theories are Available,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,49,Process Calculus,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,50,Fundament

43、al Questions,Some Fundamental Questions:What is a process?How to describe a process?What does a process do?When are two processes equivalent?No Definite Answers, Of Course!Research on the theory of process calculus

44、 proposes approximate answers,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,51,Analogy to ?-Calculus,?-Terms ? ProcessesWhat are processes?Application ? Concurrent CompositionThe fundamental operation for process calculiReductio

45、n ? CommunicationCommunications are atomic actions,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,52,The Mottos of Process Calculus,Motto 1All computing objects are processes; There are no other computing objectsMotto

46、2All computing actions are communications; There are no other kinds of actionsMotto 3A process lives to communicate,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,53,Syntactical Entities,Communications Happen through ChannelsTwo

47、Classes of Syntactic ObjectsChannelsProcesses,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,54,Three Process Calculi,CCS Calculus of Communicating SystemsMilner;1969CSP Communicating Sequential ProcessesHoare;1970?-Calculus

48、Milner,Parrow,Walker;1989,Robin Milner(1934-2010),1991 Turing AwardThree distinct and complete achievements:LCF, the mechanization of Scott's Logic of Computable Functions, probably the first theoretically based y

49、et practical tool for machine assisted proof constructionML, the first language to include polymorphic type inference together with a type-safe exception-handling mechanismCCS, a general theory of concurrency. In addit

50、ion, he formulated and strongly advanced full abstraction, the study of the relationship between operational and denotational semantics,2024年3月17日星期日,BASICS,55,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,56,Books,Communication and

51、 ConcurrencyMilner, Prentice Hall, 1989Communicating Sequential ProcessesHoare, OUP, 1980Communicating and Mobile Systems: the ?-calculusMilner, CUP, 1999The Pi-Calculus: a theory of mobile processesSangiorgi and

52、Walker, CUP, 2001,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,57,Papers,A Calculus of Mobile ProcessesThe Pioneering PaperMilner, Parrow and WalkerInformation and Computation, 1992An Introduction to the ?- CalculusJ.Parrow. C

53、hapter of Handbook of Processes Algebra. Elsevier. 2001Elements of interactionR.Milner. Communication of ACM, (Jan):78-89, 1993,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,58,Websites,Website for Mobile Processhttp://lampwww.ep

54、fl.ch/mobility/,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,59,Pure CCS,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,60,Content,SyntaxSemanticsCounter,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,61,What is CCS about?,CCS, The Calculus of Communicati

55、ng Systemsa formal language that models the operational behaviors of the communications of concurrent objects,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,62,How is CCS Defined?,The definition of CCS follows the standard approach

56、of defining a programming languageThe standard approach is widely used in computer science to define various calculi,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,63,Definition of Calculus,Defining Programming LanguagesSyntax Syn

57、tactical entityAlphabetBNF (Backus-Naur Form 巴科斯范式)SemanticsOperational behaviorLabeled Transition System, LTS,Operational Semantics,A way to give meaning to computation in a mathematically rigorous wayOther approa

58、ches to providing a formal semantics of computation include axiomatic semantics and denotational semanticsClassified into two categoriesstructural operational semantics (small-step semantics)formally describe how the

59、individual steps of a computation take place in a computer-based systemnatural semantics (big-step semantics) describe how the overall results of the executions are obtained,2024年3月17日星期日,BASICS,64,2024年3月17日星期日,上海交通大學

60、計算機系BASICS實驗室,65,Intuition about the Semantics,A = a.A’, A’ = c.A; B = c.B’, B’ = b.BExampleNa + Cl → NaCl,def,def,,,def,def,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,66,Preliminary Notations,Action,ExternalInternal,Action,E

61、xternalPotential to communicateInternal,Action,ExternalPotential to communicateInternalCommunication in a processCommunication between processes,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,70,Syntax of CCS,The abstract gramm

62、ar is defined as follows:E := 0 nil process X process variable ?.E prefix E

63、 | E’ concurrent composition E\L restriction E[f] re-labeling E + E’ non-de

64、terminism A recursionWhere ? is either a or a or ?, L ? N f: A ? A , a re-labeling function from A to ALet E be the set of process expressions and P be

65、the set of processes,,,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,71,Intuitive Explanation,0The process that can never do anything in any environmentXProcess variable?.EThe process that must first perform the action ? and th

66、en evolves as EE|E’The processes E and E’ may evlove independently or communicate through common channels,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,72,Intuitive Explanation,E\LThe process that can do whatever E may do as long

67、 as the action are not restricted by LE[f]Whatever E can do, E[f] can do with action renamed by fE+E’The process that acts either as E or as E’AThe recursive process that may never stop,2024年3月17日星期日,上海交通大學計算機系BASI

68、CS實驗室,73,What is an LTS?,E.G. automata,2024年3月17日星期日,上海交通大學計算機系BASICS實驗室,74,An Example: The ?-Calculus,Termt := x variable tt’ application ?x.t abstractionReduction(?x.t)s ? t{s/x