382V Notes for November 11

Notes.md

#EE382V/379K: Multicore Computing

##Agenda 0. Communicating Sequencer Processes 0. Temporal Logic

##Backus-Naur Form

• Developed to describe the Syntax of ALGOL
• Context-free grammar used describe the syntax of programming langauages.
• Example of a rule <symbol> ::= __expression__
• Anything in < > is a non-terminal, anything without angle brackets is terminal
• Rules are complete when everything ends in a terminal command
• Tools like YACC (Yet Another Compiler Compiler) can produce a parser when you describe a language in a Analytical Grammar (similar to BNF)

BNF rules for Guarded Command Language

This is not a comlete list of rules. Just a few rules

0. <command> ::= <simple command> | <structure command>
1. <simple command> ::= <null command> | <assignment command> | <input command> | <output command>
2. <structure command> ::= <alternative command> | <repetitive command> | <parallel command>
3. <null command> ::= skip

Program to set at most 100 numbers

s(i : 1..100)::
  *[ 
      n: integer; s(i-1)? has(n) → s(0)! false
    ▯
      [ 
        n: integer;
        s(i-1)? insert(n) → 
        *[  
            m: integer;
            s(i-1)? has(m) →
            [ 
              m ≤ n → s(0)! (m=n)
            ▯
              m > n → s(i+1)! has(m)
            ]
          ▯
            m: integer; s(i-1)? insert(m) →
            [
              m < n → s(i+1)? insert(n);n := m;
            ▯
              m = n → skip;
            ▯
              m > n → s(i+1)! has(m)
            ]
          ]
      ]
    ] 

Producer - Consumer Bounded Buffer

x:: buffer(0..9) portion;
in,out:: integer;
in:= 0;
out:= 10;
// 0 ≤ out ≤ in ≤ out+10

*[
 (in < out +10); producer ? buffer (in mod 10) → in := in + 1;
▯
 out < in; consumemr? more () →
  consumer ! buffer (out mod 10); out := out +1;
]

Temporal Logic (E. M. Clarke)

Syntax of CTL

0. Every atomic prop p ∈ AP is a CTL formula
1. If f₁ and f₂ are CTL formulas then so are

• ¬f₁
• f₁ ^ f₂
• A x f₁
• E x f₁
• A[f₁ ʋ f₂]
• E[f₁ ʋ f₂]

Semantics

Defined using M = (S, R, P)

Kripke Structure

• S: finite set of sets
• R: binary relation in S (R ⊆ S × S)
• P: S → 2^AP