-
Notifications
You must be signed in to change notification settings - Fork 59
PDGs
palvaro edited this page Mar 21, 2011
·
21 revisions
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.
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