PDGs

Predicate Dependency Graphs

Introduction

Technical Introduction

A PDG is an abstract representation of the dependency relation among BUD collections. Each collection is a node in the graph. If a collection A appears in the RHS of a rule with collection B in the LHS, we draw an arc from A to B: these arcs are annotated in various ways as described in the next section.

As does any abstract interpretation of a computer program, a PDG hides many details of the program under consideration in the hope of highlighting important details that might otherwise be obscured. In a nutshell, a PDG highlights the following:

• Dependencies among collections -- what program facts may depend on other program facts?
• Temporal dependencies -- what deductions require the passage of (logical) time?
• Nonmonotonicity -- which deductions are potentially defeasible, tentative or order-sensitive?
• Asynchrony -- which deductions cross network network boundaries (and hence become true at an unknown time)?

Notably, PDGs ignore the following details of a program:

• Rule identity -- if two rules r1 and r2 define A in terms of B, both rules may be collapsed into one arc B -> A.
• Schema -- the granularity of a PDG is collection.
• Data transformations -- any column data that is transformed or generated in a rule RHS is not accounted for (due to the previous).

The PDG abstraction provides an over-approximation of the dependency relation.

Intuition

Reading a PDG

Legend

A simple BUD abstract interface and a concrete implementation

module DeliveryProtocol
  state do
    interface input, :pipe_in, [:dst, :src, :ident] => [:payload]
    interface output, :pipe_sent, [:dst, :src, :ident] => [:payload]
  end
end

module BestEffortDelivery
  include DeliveryProtocol

  state do
    channel :pipe_chan, [:@dst, :src, :ident] => [:payload]
  end

  bloom :snd do
    pipe_chan <~ pipe_in
  end

  bloom :done do
    pipe_sent <= pipe_in
  end
end

Their PDGs

Interpreting a PDG