Periodic-Drop-Take Calculus for Stream Transformers (based on CS-Report

Periodic-Drop-Take Calculus for Stream Transformers (based on CS-Report

Periodic-Drop-Take Calculus for Stream Transformers (based on CS-Report 05-02) Rudolf Mak January 21, 2005 Feb 3, 2020 Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking

1 Motivation For stream processing systems build in a LEGOlike fashion from a fixed set of building blocks we want to specify verify analyze their functional behavior. Moreover we want to design systems of specified functionality. Feb 3, 2020

Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking 2 Question What does this system compute for various values of k? Feb 3, 2020

Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking 3 Periodic Stream samplers Feb 3, 2020 Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking

4 PDT-calculus Operators Drop operators Take operators Equational rules

Drop expansion/contraction Drop exchange Complement Drop elimination/Introduction Take composition Feb 3, 2020 Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking

5 Drop operator Feb 3, 2020 Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking 6

Canonical forms 1. Period-consecutive 2. Rank-increasing 3. Primitive X Feb 3, 2020 Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking 7

Drop expansion/contraction rule Feb 3, 2020 Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking 8 Example

q-fold Feb 3, 2020 Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking (l+1)-fold 9 Drop exchange rule

Feb 3, 2020 Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking 10 Completeness Feb 3, 2020

Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking 11 Rewriting to canonical form Feb 3, 2020 Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking

12 Take operator Feb 3, 2020 Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking 13 Complement

Feb 3, 2020 Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking 14 Rules involving take operators Drop elimination/introduction Take composition

Feb 3, 2020 Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking 15 Split component Feb 3, 2020

Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking 16 Merge component Feb 3, 2020 Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking

17 Block reverser Feb 3, 2020 Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking 18 Split-merge systems

Feb 3, 2020 Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking 19 The set of equations Esv Feb 3, 2020

Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking 20 Solving a single equation 1 Arbitrary shape Canonical shape Period-aligned, pseudo-canonical shape

Feb 3, 2020 Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking 21 Solving a single equation 2 Feb 3, 2020 Rudolf Mak [email protected]

TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking 22 Example Feb 3, 2020 Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking 23

Esv theorem for SISO systems Feb 3, 2020 Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking 24 Split component

Feb 3, 2020 Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking 25 Emv theorem for SISO systems Feb 3, 2020 Rudolf Mak [email protected]

TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking 26 Question revisited What does this system compute for various values of k? Feb 3, 2020 Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking

27 Answer k = 0, junk, irreparable deadlock k = 1, 2-place buffer

k = 2, block reverser with block size 2 Feb 3, 2020 Rudolf Mak [email protected] TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking 28 Conclusions PDT-calculus is a simple calculus to reason about periodically sampled streams.

PDT-calculus is sound and complete. Semantic model in the form of a monoid. Algorithm to determine canonical forms (solves the word problem). Algorithm to solve linear equations in a single variable (solves the division problem). Functionality of arbitrary SISO-systems can be analyzed. Only partial correctness is addressed. Feb 3, 2020 Rudolf Mak [email protected]

TU/e, Dept. of Math. and Comp. Sc., System Architecture and Networking 29

Recently Viewed Presentations

  • Genomic selection and systems biology - lessons from dairy ...

    Genomic selection and systems biology - lessons from dairy ...

    AIP objectives. Expand national and international collection of phenotypic and genotypic data. Develop a more accurate genomic evaluation system with advanced, efficient methods to combine pedigrees, genotypes, and phenotypes
  • Ch 4.3 Succession

    Ch 4.3 Succession

    Cellular Boundaries. Cell Membrane. Consists of a lipid bilayer, a strong but flexible barrier between the cell and its surroundings. The cell membrane regulates what enters and leaves the cell and also protects and supports the cell. Most biological membranes...
  • Usability Basics for the Information Professional Uta Hussong-Christian

    Usability Basics for the Information Professional Uta Hussong-Christian

    edited by Nancy Fried Foster and Susan Gibbons. This is the study where they used ethnographic methods to learn about students' work practices and then applied what they found to their web site redesign.
  • Site Visit - Academics

    Site Visit - Academics

    Site Visit Preparation Assignment As a group, meet with a business and learn about its form of ownership mission, ethical guidelines organizational structure management basic marketing strategies. Prepare a written, single-spaced memo addressing the above (see guidelines for writing memo...
  • Environmental "Law" and Globalization

    Environmental "Law" and Globalization

    Do the higher levels-- Hard Law/Soft Law Some forms of international law: General approaches to the relationship between domestic and international law Ways in which international agreements can find their way into domestic law If an international norm isn't "hard"...
  • Bloodborne Pathogens Training - University of Michigan-Flint

    Bloodborne Pathogens Training - University of Michigan-Flint

    Course Information. This bloodborne pathogens training program is required annually for UM employees who may reasonably anticipate contact with blood or other potentially infectious materials (OPIM), during the performance of their duties.
  • TCP Congestion Control - WPI

    TCP Congestion Control - WPI

    Modified Slow Start With fast recovery, slow start only occurs: At cold start After a coarse-grain timeout This is the difference between TCP Tahoe and TCP Reno!! TCP Congestion Control TCP Congestion Control Essential strategy :: The TCP host sends...
  • Pengantar Teknologi Informasi

    Pengantar Teknologi Informasi

    PENGANTAR TEKNOLOGI INFORMASI Diat Nurhidayat, M.Ti PTIK FT-UNJ * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *...