WG211/M24Blazy - Revision history

Sandrine at 13:48, 27 November 2024

2024-11-27T13:48:13Z

← Older revision		Revision as of 15:48, 27 November 2024
Line 1:		Line 1:
	This talk proposes a mechanized formal semantics for		This talk proposes a mechanized formal semantics for dataflow circuits:
	dataflow circuits: rather than following a static schedule		rather than following a static schedule predetermined at generation time,
	predetermined at generation time, the execution of the components in		the execution of the components in a circuit is constrained solely by the availability of their input data.
	a circuit is constrained solely by the availability of their input
	data.
	We model circuit components as abstract computing units,		We model circuit components as abstract computing units,
	asynchronously connected with each other through unidirectional,		asynchronously connected with each other through unidirectional,
Line 21:		Line 19:
	We prove that both representations are semantically equivalent.		We prove that both representations are semantically equivalent.

	We conduct our formalization within the Coq proof assistant. We experimentally validate its relevance by applying our general semantic framework to dataflow circuits generated with Dynamatic, a recent HLS tool exploiting dataflow circuits to generate dynamically scheduled, elastic circuits.		We conduct our formalization within the Coq proof assistant. We experimentally
			validate its relevance by applying our general semantic framework to dataflow circuits
			generated with Dynamatic, a recent HLS tool exploiting dataflow circuits to generate dynamically scheduled, elastic circuits.

Sandrine at 13:45, 27 November 2024

2024-11-27T13:45:51Z

← Older revision		Revision as of 15:45, 27 November 2024
Line 20:		Line 20:
	constructing and reasoning about circuits in a inductive way.		constructing and reasoning about circuits in a inductive way.
	We prove that both representations are semantically equivalent.		We prove that both representations are semantically equivalent.


	We conduct our formalization within the Coq proof assistant. We experimentally validate its relevance by applying our general semantic framework to dataflow circuits generated with Dynamatic, a recent HLS tool exploiting dataflow circuits to generate dynamically scheduled, elastic circuits.		We conduct our formalization within the Coq proof assistant. We experimentally validate its relevance by applying our general semantic framework to dataflow circuits generated with Dynamatic, a recent HLS tool exploiting dataflow circuits to generate dynamically scheduled, elastic circuits.

Sandrine: Created page with " This talk proposes a mechanized formal semantics for dataflow circuits: rather than following a static schedule predetermined at generation time, the execution of the com..."

2024-11-27T13:45:22Z

Created page with " This talk proposes a mechanized formal semantics for dataflow circuits: rather than following a static schedule predetermined at generation time, the execution of the com..."

New page

This talk proposes a mechanized formal semantics for
dataflow circuits: rather than following a static schedule
predetermined at generation time, the execution of the components in
a circuit is constrained solely by the availability of their input
data.
We model circuit components as abstract computing units,
asynchronously connected with each other through unidirectional,
unbounded FIFO. In contrast to Kahn's classic, denotational semantic
framework, our semantics is operational. It intends to reflect
Dennis' dataflow paradigm with firing, while still formalizing the
observable behaviors of circuits as channels histories.

The components we handle are either stateless or stateful, and may
be non-deterministic. We formalize sufficient conditions to achieve
the determinacy of circuits executions: all possible schedules of
such circuits lead to a unique observable behavior.
We provide two equivalent views for circuits. The first one is a
direct and natural representation as graphs of components. The
second is a core, structured term calculus, which enables
constructing and reasoning about circuits in a inductive way.
We prove that both representations are semantically equivalent.

We conduct our formalization within the Coq proof assistant. We experimentally validate its relevance by applying our general semantic framework to dataflow circuits generated with Dynamatic, a recent HLS tool exploiting dataflow circuits to generate dynamically scheduled, elastic circuits.