Safe Haskell | Safe-Inferred |
---|---|
Language | GHC2021 |
This module contains the type definitions and basic operations for the graph that Futhark.Optimise.ReduceDeviceSyncs.MigrationTable internally uses to construct a migration table. It is however completely Futhark-agnostic and implements a generic graph abstraction.
Overview
The Graph
type is a data flow dependency graph of program variables, each
variable represented by a Vertex
. A vertex may have edges to other vertices
or to a sink, which is a special vertex with no graph representation. Each
edge to a vertex is either from another vertex or from a source, which also
is a special vertex with no graph representation.
The primary graph operation provided by this module is route
. Given the
vertex that some unspecified source has an edge to, a path is attempted
found to a sink. If a sink can be reached from the source, all edges along
the path are reversed. The path in the opposite direction of reversed edges
from a source to some sink is a route.
Routes can be used to find a minimum vertex cut in the graph through what amounts to a specialized depth-first search implementation of the Ford-Fulkerson method. When viewed in this way each graph edge has a capacity of 1 and the reversing of edges to create routes amounts to sending reverse flow through a residual network (the current state of the graph). The max-flow min-cut theorem allows one to determine a minimum edge cut that separates the sources and sinks.
If each vertex v
in the graph is viewed as two vertices, v_in
and
v_out
, with all ingoing edges to v
going to v_in
, all outgoing edges
from v
going from v_out
, and v_in
connected to v_out
with a single
edge, then the minimum edge cut of the view amounts to a minimum vertex cut
in the actual graph. The view need not be manifested as whether v_in
or
v_out
is reached by an edge to v
can be determined from whether that edge
is reversed or not. The presence of an outgoing, reversed edge also gives the
state of the virtual edge that connects v_in
to v_out
.
When routing fails to find a sink in some subgraph reached via an edge then that edge is marked exhausted. No sink can be reached via an exhausted edge, and any subsequent routing attempt will skip pathfinding along such edge.
Synopsis
- data Graph m
- type Id = Int
- type IdSet = IntSet
- data Vertex m = Vertex {
- vertexId :: Id
- vertexMeta :: m
- vertexRouting :: Routing
- vertexEdges :: Edges
- data Routing
- data Exhaustion
- data Edges
- data EdgeType
- data Visited a
- data Result a
- empty :: Graph m
- vertex :: Id -> m -> Vertex m
- declareEdges :: [Id] -> Edges
- oneEdge :: Id -> Edges
- none :: Visited a
- insert :: Vertex m -> Graph m -> Graph m
- adjust :: (Vertex m -> Vertex m) -> Id -> Graph m -> Graph m
- connectToSink :: Id -> Graph m -> Graph m
- addEdges :: Edges -> Id -> Graph m -> Graph m
- member :: Id -> Graph m -> Bool
- lookup :: Id -> Graph m -> Maybe (Vertex m)
- isSinkConnected :: Id -> Graph m -> Bool
- route :: Id -> Graph m -> (Maybe Id, Graph m)
- routeMany :: [Id] -> Graph m -> ([Id], Graph m)
- fold :: Graph m -> (a -> EdgeType -> Vertex m -> a) -> (a, Visited ()) -> EdgeType -> Id -> (a, Visited ())
- reduce :: Monoid a => Graph m -> (a -> EdgeType -> Vertex m -> a) -> Visited (Result a) -> EdgeType -> Id -> (Result a, Visited (Result a))
Types
A data flow dependency graph of program variables, each variable
represented by a Vertex
.
A graph representation of some program variable.
Vertex | |
|
Route tracking for some vertex. If a route passes through the vertex then both an ingoing and an outgoing edge to/from that vertex will have been reversed, and the vertex will in effect have lost one edge and gained another. The gained edge will be to the prior vertex along the route that passes through.
NoRoute | No route passes through the vertex, and no edges have been reversed, added, nor deleted compared to what was declared. |
FromSource | A route passes through the vertex, and the prior vertex is the source of that route. The edge gained by reversal is by definition exhausted. |
FromNode Id Exhaustion | A route passes through the vertex, and this is the handle of the prior
vertex. The edge gained by reversal may be exhausted. Routing assumes
that at most one |
data Exhaustion Source #
Whether some edge is exhausted or not. No sink can be reached via an exhausted edge.
Instances
Show Exhaustion Source # | |
Defined in Futhark.Optimise.ReduceDeviceSyncs.MigrationTable.Graph showsPrec :: Int -> Exhaustion -> ShowS # show :: Exhaustion -> String # showList :: [Exhaustion] -> ShowS # | |
Eq Exhaustion Source # | |
Defined in Futhark.Optimise.ReduceDeviceSyncs.MigrationTable.Graph (==) :: Exhaustion -> Exhaustion -> Bool # (/=) :: Exhaustion -> Exhaustion -> Bool # | |
Ord Exhaustion Source # | |
Defined in Futhark.Optimise.ReduceDeviceSyncs.MigrationTable.Graph compare :: Exhaustion -> Exhaustion -> Ordering # (<) :: Exhaustion -> Exhaustion -> Bool # (<=) :: Exhaustion -> Exhaustion -> Bool # (>) :: Exhaustion -> Exhaustion -> Bool # (>=) :: Exhaustion -> Exhaustion -> Bool # max :: Exhaustion -> Exhaustion -> Exhaustion # min :: Exhaustion -> Exhaustion -> Exhaustion # |
All relevant edges that have been declared from some vertex, plus bookkeeping to track their exhaustion and reversal.
ToSink | The vertex has an edge to a sink; all other declared edges are
irrelevant. The edge cannot become exhausted, and it is reversed if a
route passes through the vertex ( |
ToNodes IdSet (Maybe IdSet) | All vertices that the vertex has a declared edge to, and which of those edges that are not exhausted nor reversed, if not all. |
Whether a vertex is reached via a normal or reversed edge.
State that tracks which vertices a traversal has visited, caching immediate computations.
The result of a graph traversal that may abort early in case a sink is reached.
Produced a | The traversal finished without encountering a sink, producing this value. |
FoundSink | The traversal was aborted because a sink was reached. |
Construction
declareEdges :: [Id] -> Edges Source #
Creates a set of edges where no edge is reversed or exhausted.
Insertion
insert :: Vertex m -> Graph m -> Graph m Source #
Insert a new vertex into the graph. If its variable already is represented in the graph, the original graph is returned.
Update
adjust :: (Vertex m -> Vertex m) -> Id -> Graph m -> Graph m Source #
Adjust the vertex with this specific id. When no vertex with that id is a member of the graph, the original graph is returned.
connectToSink :: Id -> Graph m -> Graph m Source #
Connect the vertex with this id to a sink. When no vertex with that id is a member of the graph, the original graph is returned.
addEdges :: Edges -> Id -> Graph m -> Graph m Source #
Add these edges to the vertex with this id. When no vertex with that id is a member of the graph, the original graph is returned.
Query
isSinkConnected :: Id -> Graph m -> Bool Source #
Returns whether a vertex with the given id exists in the graph and is connected directly to a sink.
Routing
route :: Id -> Graph m -> (Maybe Id, Graph m) Source #
route src g
attempts to find a path in g
from the source connected
vertex with id src
. If a sink is found, all edges along the path will be
reversed to create a route, and the id of the vertex that connects to the
sink is returned.
routeMany :: [Id] -> Graph m -> ([Id], Graph m) Source #
routeMany srcs g
attempts to create a route
in g
from every vertex
in srcs
. Returns the ids for the vertices connected to each found sink.
Traversal
fold :: Graph m -> (a -> EdgeType -> Vertex m -> a) -> (a, Visited ()) -> EdgeType -> Id -> (a, Visited ()) Source #
fold g f (a, vs) et i
folds f
over the vertices in g
that can be
reached from the vertex with handle i
accessed via an edge of type et
.
Each vertex v
may be visited up to two times, once for each type of edge
e
pointing to it, and each time f a e v
is evaluated to produce an
updated a
value to be used in future f
evaluations or to be returned.
The vs
set records which f a e v
evaluations already have taken place.
The function returns an updated Visited
set recording the evaluations it
has performed.
reduce :: Monoid a => Graph m -> (a -> EdgeType -> Vertex m -> a) -> Visited (Result a) -> EdgeType -> Id -> (Result a, Visited (Result a)) Source #
reduce g r vs et i
returns FoundSink
if a sink can be reached via the
vertex v
with id i
in g
. Otherwise it returns Produced
(r x et v)
where x
is the <>
aggregate of all values produced by reducing the
vertices that are available via the edges of v
.
et
identifies the type of edge that v
is accessed by and thereby which
edges of v
that are available. vs
caches reductions of vertices that
previously have been visited in the graph.
The reduction of a cyclic reference resolves to mempty
.