futhark-0.25.9: An optimising compiler for a functional, array-oriented language.
Safe HaskellSafe-Inferred
LanguageGHC2021

Futhark.Optimise.ReduceDeviceSyncs.MigrationTable.Graph

Description

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

Types

data Graph m Source #

A data flow dependency graph of program variables, each variable represented by a Vertex.

type Id = Int Source #

A handle that identifies a specific Vertex.

type IdSet = IntSet Source #

A set of Ids.

data Vertex m Source #

A graph representation of some program variable.

Constructors

Vertex 

Fields

data Routing Source #

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.

Constructors

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 FromNode routing exists to each vertex in a graph.

data Edges Source #

All relevant edges that have been declared from some vertex, plus bookkeeping to track their exhaustion and reversal.

Constructors

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 (vertexRouting v /= NoRoute).

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.

data EdgeType Source #

Whether a vertex is reached via a normal or reversed edge.

Constructors

Normal 
Reversed 

data Visited a Source #

State that tracks which vertices a traversal has visited, caching immediate computations.

data Result a Source #

The result of a graph traversal that may abort early in case a sink is reached.

Constructors

Produced a

The traversal finished without encountering a sink, producing this value.

FoundSink

The traversal was aborted because a sink was reached.

Instances

Instances details
Semigroup a => Semigroup (Result a) Source # 
Instance details

Defined in Futhark.Optimise.ReduceDeviceSyncs.MigrationTable.Graph

Methods

(<>) :: Result a -> Result a -> Result a #

sconcat :: NonEmpty (Result a) -> Result a #

stimes :: Integral b => b -> Result a -> Result a #

Eq a => Eq (Result a) Source # 
Instance details

Defined in Futhark.Optimise.ReduceDeviceSyncs.MigrationTable.Graph

Methods

(==) :: Result a -> Result a -> Bool #

(/=) :: Result a -> Result a -> Bool #

Construction

empty :: Graph m Source #

The empty graph.

vertex :: Id -> m -> Vertex m Source #

Constructs a Vertex without any edges.

declareEdges :: [Id] -> Edges Source #

Creates a set of edges where no edge is reversed or exhausted.

oneEdge :: Id -> Edges Source #

Like declareEdges but for a single vertex.

none :: Visited a Source #

Initial Visited state before any vertex has been visited.

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

member :: Id -> Graph m -> Bool Source #

Does a vertex for the given id exist in the graph?

lookup :: Id -> Graph m -> Maybe (Vertex m) Source #

Returns the vertex with the given id.

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.