Theory of Parallel Computing


Course Overview: This course will cover all the topics mentioned below

·         Circuit model of computation
o    presentation and discussion
o    metrics: work, depth, speedup, efficiency
o    Brent's theorem
·         IO complexity and pebbling games
o    Red/blue pebbling, lower bounds
o    Simple model of communication complexity, lower bounds
o    Graph properties, expanders, bisection...
·         Algebraic circuits
o    reduction and parallel prefix circuits
·         PRAM model
o    linked list parallel prefix and symmetry breaking
·         postal model, LogP model and variations
o    collective communication
·         Packet-routing algorithms
·         Toplogy-specific algorithms (butterflies, hypercubes and meshes)
o    sorting and routing
·         Coordination with shared memory
o    work stealing
o    distributed coordination , diffracting trees, sorting networks
·         Possible additions
o    PRAM simulation on networks
o    NESL simulation
o    Systolic algorithms
o    Complexity classes, P and NC
o    Quantum computing

Download PDF Lectures

  1. Lecture 1 Aug 24th  Circuits, Brent Theorem, Communication complexity
  2. Lecture 2 Aug 26th  Communication Complexity
  3. Lecture 3 Aug 31st Algebraic circuits, reduction and scan
  4. Lecture 4 Sept 2, lower bounds on scan, optimal depth scan
  5. Lecture 5, Sept 7, Existence of expanders.
  6. Lecture 6, Sept 9. Expanders and linear algebra
  7. Lecture 7, Sept 16. PRAM, APRAM
  8. Lecture 8, Sept 21st. Scan on linked list
  9. Lecture 9, Sept 23rd. Optimal deterministic scan
  10. Lecture 10, Sept 28th, Complete proof (rebalancing with expanders)
  11. Lecture 11, Sept 30, PRAM algorithms -- connectivity
  12. Lecture 12, Oct 5th, Communication complexity (I/O complexity)
  13. Lecture 13, Oct 7th, Communication complexity (permutations, sorting, transpose, FFT)
  14. Lecture 14, Oct 12th., Sorting Networks
  15. Lecture 15th, Oct 14th, AKS Sorting Network
  16. Lecture 16th, Oct 19th, Cole's logarithmic sorting
  17. Lecture 17th Oct 21st. Routing, l.b. on deterministic routing
  18. Lecture 18th, Oct 26th, Randomized routing
  19. Lecture 19th Oct 28th, Nov 2  Butterfly randomized sorting
  20. Lecture 20 Nov 9-11th, VLSI Complexity
  21. Lecture 21, Nov 30th-Dec 2nd Work Stealing

Logical Foundation of Computer Science


Course Overview:
Logic is one of the corner stones of computer science. Logic plays a crucial role in diverse areas of computer science such as architechture (logic gates), software engineering (specification and verification), programming languages (semantics, logic programming), databases (relational databases, SQL, XML processing), artificial intelligence (automatic theorem proving, inductive reasoning), algorithms (complexity and expressiveness), and theory of computation (general notions of computability).

This course will provide an introduction to mathematical logic from the perspective of computer science, emphasizing decidable fragments of logic and decision algorithms. The topics covered will be motivated by applications in artificial intelligence, databases, formal methods and theoretical computer science. The goal of the course is to prepare students for using logic as a formal tool in computer science. The course will roughly cover the following topics (in this order): syntax, semantics and proof theory of propositional logic, sat-solvers, syntax of first-order, the resolution proof system, syntax of second-order logic, connections between monadic second order logic and regular languages (word and tree, finite and infinite), tree-width and Courcelle's theorem with applications to parametric complexity, finite model theory and descriptive complexity, games and inexpressiveness.


Logic in Computer Science


Lec#
Topic
Slides PDF/PPT
1
Course overview and logistics; 
 A brief history of logic
2
Propositional logic -- syntax and semantics; Konig's Lemma
Lecture #2 -  
    Slides (PDF) 
    Printable (PDF)
3
Proof systems for propositional logic: 
  Resolution proof system, 
  A Hilbert/Frege style proof system, 
  Soundness of these systems
Lecture #3 - 
    Slides (PDF) 
    Printable (PDF)
4
Propositional logic: 
  Hintikka's lemma, 
  Model-existence theorem
Lecture #4 -  
     Slides (PDF) 
     Printable (PDF)
5
Compactness theorem: 
    Two proofs: One using Model-existence theorem; 
        one using Konig's lemma.

Lecture# 5: 
    Lost due to computer crash!
6
Propositional Consequence/Strong Completeness Theorem 
   for Resolution. 
The Advent of SAT solver technology: history, DPLL, conflict clause 
learning, and modern SAT solvers.
Lecture #6: 
Strong Completeness:  
     Slides (PDF) 
     Printable (PDF)
7
Review of automata theory, computability and complexity theory. 
Cook-Levin theorem (SAT is NP-complete) and its proof.
Lecture #7: 
Review of automata, computability and complexity 
(Mahesh's notes): 
    Slides (PDF) 
    Printable (PDF) 

Cook-Levin Theorem and some 
 interesting complexity 
 theory results: 
    Slides (PDF) 
    Printable (PDF)
8
First-order logic: Syntax and semantics; 
 Equality
Lecture #8: 
    Slides (PDF) 
    Printable (PDF)
9 
10
First Order Logic: 
   Hintikka's Lemma 
   Model-existence Theorem 
   Resolution: Soundness & Completeness
Lectures #9 and #10: 
    Slides (PDF) 
    Printable (PDF)
11
Church-Turing Theorem: 
   Validity of FOL is undecidable. 
Godel's incompleteness theorem (first)
Lecture #11: 
    Slides (PDF) 
    Printable (PDF)
12 
13
Second-order logics 
 Monadic second-order logics 
 MSO over words and Regular Languages
Lecture #12 and #13: 
    Slides (PDF)
14
Interpretations: 
   Deciding FOL(N,+,0,1) by interpretation 
          on MSO(N, succ). 
   Deciding FOL over infinite trees by 
          interpretation on MSO(N, succ)
Lecture #14: 
    Slides (PDF)
15
Monadic Second Order Logic 
   on finite trees 
 MSO and regular tree languages  
 MSO on infinite trees; 
 Rabin's theorem: 
   MSO over infinite trees is decidable
Lecture #15: 
    Slides (PDF)
16
Decidability of emptiness of tree automata; solving finite-state games; brief sketch of checking emptiness of automata on infinite trees.
Lecture #16: 
   Slides (PDF) 
17
MSO interpretations: 
  Decidability of MSO on n-ary trees; 
  Decidability of MSO on series-parallel 
       graphs.
Lecture #17: 
   Slides (PDF)
18
More interpretations: 
 Decidability of MSO on pushdown graphs 
 Decidability of FO on automatic graphs 
    (part 1)
Lecture #18: 
   Slides (PDF)
19
Decidability of FO on automatic graphs (part II) 
 FO of reals with addition and multiplication 
   is decidable (Tarski) 
 Quantifier elimination 
Lecture #19: 
   Slides (PDF)
20
Finite model theory I: 
   Review of classical logic. 
   Failiure of fundamental theorems in finite model theory: 
compactness theorem fails, valid sentences not in r.e.        (Trakhtenbrot's theorem) 
The three themes: 
   1. Logic and compexity theory 
   2. (In)expressivess of logics, EF games 
   3. Classical theorems reevaluated in 
          the finite model setting.
Lecture #20: 
   Slides (PDF)
21  
22
Finite model theory: 
   Ehrenfeucht-Fraisse Games 
   Quantifier rank 
   EVEN not expressible in FOL 
   CONNECTED not expressible in FOL 
   Proof of EF-theorem; Rank-k types 
    
Lecture #21 & #22:  
   Slides (PDF)
23
Finite model theory: 
   - Fagin's theorem  ESO=NP
Lecture #23:  
   Slides (PDF)
24
Finite model theory: 
   - Fagin's theorem continued 
   - Fixed point logics 
        * Monotonic & inflationary operators 
        * FO + LFP
Lecture #24: 
   Slides (PDF)
25
Finite model theory (concluding) 
    - FO+LFP = P (no proof) 
    - FO+PFP = PSPACE (no proof) 
    - EMSO notequals AMSO on structures 
                         (no proof) 

Courcelle's theorem: 
    - Embedding graphs in trees 
         (examples) 
    - Definition of tree-width

Lecture #25:  
   Slides (PDF)
26
Fixed-parameter tractability 
Courcelle's theorem 
  - Any MSO property on finite graphs of 
      bounded tree-width can be 
      model-checked in linear time. 
Lecture #26:  
     Slides (PDF)
FALL BREAK - NO CLASS

FALL BREAK - NO CLASS

27, 28
Review of topics and results; 
Also SMT solvers
Lecture #27, Lecture #28 
      Slides (PDF)
free counters