From 258ae7730d7556ba22fee0f800a90a19f077f237 Mon Sep 17 00:00:00 2001 From: Minseong Jang Date: Mon, 14 Oct 2024 11:54:31 +0900 Subject: [PATCH] Update dependency types section in book --- doc/docs/advanced/dependency.md | 154 ++++- .../figure/dependency-comb-loop-detection.svg | 396 +++++++++++ doc/docs/figure/dependency-comb-loop.svg | 386 +++++++++++ doc/docs/figure/dependency-limitations.svg | 616 ++++++++++++++++++ doc/docs/figure/dependency-map-resolver.svg | 316 +++++++++ doc/docs/figure/dependency-sink.svg | 196 ++++++ doc/docs/figure/dependency-source.svg | 196 ++++++ doc/docs/lang/signal.md | 2 +- 8 files changed, 2251 insertions(+), 11 deletions(-) create mode 100644 doc/docs/figure/dependency-comb-loop-detection.svg create mode 100644 doc/docs/figure/dependency-comb-loop.svg create mode 100644 doc/docs/figure/dependency-limitations.svg create mode 100644 doc/docs/figure/dependency-map-resolver.svg create mode 100644 doc/docs/figure/dependency-sink.svg create mode 100644 doc/docs/figure/dependency-source.svg diff --git a/doc/docs/advanced/dependency.md b/doc/docs/advanced/dependency.md index 397f41c..5c6b441 100644 --- a/doc/docs/advanced/dependency.md +++ b/doc/docs/advanced/dependency.md @@ -3,15 +3,46 @@ We defined the "dependency type" based on the dependency from the backward signal to the forward signal. The concept was inspired from the [BaseJump STL](https://dl.acm.org/doi/pdf/10.1145/3195970.3199848). -It has two kinds of dependency types: `Helpful` and `Demanding`. +## Motivation: Combinational Loop -- `Helpful`: forward signals does not depend on the backward signals. -- `Demanding`: forward signals depends on the backward signals, and they satisfy the condition that if the payload is `Some`, the ready condition is true. +The following circuit is constructed by connecting [`source`](../lang/combinator.md#source), [`map_resolver`](../lang/combinator.md#map_resolver), and [`sink`](../lang/combinator.md#sink) combinators. -> Note that the dependency type does not consider the inter-interface backward dependency. -It is exposed in the IO types for `lfork` combinator. +

+ +

-It is defined as variants of an enum `Dep`: +```rust,noplayground +fn m() { + I::, Opt>>::source() + .map_resolver::>(|p: Ready>| p.inner.unwrap_or(0)) + .sink() +} +``` + +In this circuit, we can consider the dependency between the `f2` and `b2` signals from two perspectives: + +- Since the `source` combinator forwards the backward signals to the forward signals and the `map_resolver` combinator preserves the dependencies between its forward and backward signals, there is a dependency `b2 -> b1 -> f1 -> f2`. +- Since the `sink` combinator forwards the forward signals to the backward signals, there is a dependency `f2 -> b2`. + +Thus, a cyclic dependency exists between `f2` and `b2`. +This is commonly referred to as a *combinational loop*, which makes the circuit never stabilize and causes the simulator to hang. +A combinational loop occurs when the output of some combinational logic is fed back into the input of that same combinational logic without any intervening register. + +## Dependency Types + +To prevent combinational loops in circuit design, we use a type system called "Dependency Type". + +We categorize interfaces into two kinds of types: `Helpful` and `Demanding`. + +- `Helpful`: forward signals does not depend on its backward signals. +- `Demanding`: forward signals depends on its backward signals, and they satisfy the condition that if the payload is `Some`, the ready condition is true. + +Based on the above definition, in the motivational circuit, both the interface between `source` and `map_resolver` and the interface between `map_resolver` and `sink` are of the `Demanding` type. + +> NOTE: In our type system, we do not consider the case where the forward signals depend on the backward signals, the payload is `Some`, but the ready condition is false. +This case is guaranteed not to occur when the circuit is designed only with the combinator defiend in our standard combinator library. + +In HazardFlow, we defined the dependency type as an enum `Dep`: ```rust,noplayground /// Dependency type of a hazard interface. @@ -28,7 +59,7 @@ enum Dep { } ``` -We annotate the dependency type to the hazard interface. +and we annotated the dependency type to the hazard interface. ```rust,noplayground /// Hazard interface. @@ -36,13 +67,115 @@ We annotate the dependency type to the hazard interface. struct I; ``` -The benefit of using dependency type is that it is useful to guarantee the transfer happens or not in the interface. -We will explain more with the example implementation of interface combinators. +The benefit of using dependency types is that we can restrict the usage of combinators that introduce a combinational loop, which leads to more productive circuit design. +We will explain more with the example of interface combinators. ## Examples: Types for Interface Combinators -The most common example of dependency type is the IO of interface combinators. +Let's look into the IO type for the interface combinators in the motivational circuit. + +### `source` + +

+ +

+ +```rust,noplayground +impl I, { Dep::Demanding }> { + fn source() -> I, { Dep::Demanding }> { + ().fsm::, { Dep::Demanding }>, ()>((), |_, er, _| { + let ep = if er.ready { Some(er.inner) } else { None }; + (ep, (), ()) + }) + } +} +``` + +Since the forward signals (`ep`) depend on the backward signals (`er`), its egress interface has a `Demanding` type. +Therefore, it returns an `I, { Dep::Demanding }>`. + +### `map_resolver` + +

+ +

+ +```rust,noplayground +impl I, D> { + fn map_resolver(self, f: impl Fn(Ready) -> R) -> I, D> { + self.fsm::, D>, ()>(|ip, er, _| { + let ep = ip; + let ir = Ready::new(er.ready, f(er)); + (ep, ir, ()) + }) + } +} +``` + +The egress forward signals (`ep`) depend on the ingress forward signals (`ip`), +while ingress backward signals (`ir`) depend on the egress backward signals (`er`). +Therefore, if the ingress interface has a `Helpful` type (`ir -/-> ip`), +then the egress interface will also have a `Helpful` type (`er -> ir -/-> ip -> ep`). +Similarly, if the ingress interface has a `Demanding` type, then the egress interface will also have a `Demanding` type. +Consequently, it takes an `I, D>` and returns an `I, D>`, where `D` can be any type. + +### `sink` + +

+ +

+ + +```rust,noplayground +impl I>, { Dep::Helpful }> { + fn sink(self) { + self.fsm::<(), ()>((), |ip, _, _| { + let ir = Ready::valid(ip); + ((), ir, ()) + }) + } +} +``` + +Since the backward signals (`ir`) depend on the forward signals (`ip`), +a combinational loop occurs when the ingress interface has a `Demanding` type (`ir` -> `ip` -> `ir`). +To prevent this, we only allow the ingress interface to have a `Helpful` type. +Therefore, it takes only `I>, { Dep::Helpful }>`. + +Now let's apply the combinator types introduced above to the motivational circuit. + +

+ +

+ +The egress interface of `source` combinator is `I, { Dep::Demanding }>`, +and the egress interface of `map_resolver` combinator is `I>, { Dep::Demanding }>`. +However, since the `sink` combinator only takes ingress interface of `Helpful` type, +we cannot apply the `sink` combinator to the egress interface of `map_resolver`. +This prevents the occurrence of combinational loops. +To apply the `sink` combinator, we need to change the type to `Helpful` by using combinators like [`reg_fwd`](../lang/combinator.md#reg_fwd). + +## Limitations + +Currently, a limitation exists in that dependency types cannot capture all types of combinational loops. +This is because dependency types only check for intra-interface dependencies and do not consider for inter-interface dependencies. +The most common example of this is the `fork-join` pattern. + +

+ +

+ +In the circuit described above, a combinational loop exists with `f1 -> b2 -> f1` and `f2 -> b1 -> f2`. +However, the current type system cannot detect such loops. +For the `lfork` combinator, since there is no dependency from `b1 -> f1` or `b2 -> f2`, if the ingress interface type is `Helpful`, then both egress interface types will also be `Helpful`. + +And for the `join` combinator, it is designed to take two `Helpful` ingress interfaces (let's call them `i1` and `i2`) and return a `Helpful` egress interface. +However, a combinational loop occurs if there is a dependency from the backward signals of `i1` to the forward signals of `i2`, or from the backward signals of `i2` to the forward signals of `i1`. + +Since the current type system cannot represent inter-interface dependencies, this remains as a limitation. +For now, we expect that these types of combinational loops will be detected by synthesis tools. + diff --git a/doc/docs/figure/dependency-comb-loop-detection.svg b/doc/docs/figure/dependency-comb-loop-detection.svg new file mode 100644 index 0000000..a292648 --- /dev/null +++ b/doc/docs/figure/dependency-comb-loop-detection.svg @@ -0,0 +1,396 @@ + + + + + + image/svg+xml + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/doc/docs/figure/dependency-comb-loop.svg b/doc/docs/figure/dependency-comb-loop.svg new file mode 100644 index 0000000..2993be2 --- /dev/null +++ b/doc/docs/figure/dependency-comb-loop.svg @@ -0,0 +1,386 @@ + + + + + + image/svg+xml + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/doc/docs/figure/dependency-limitations.svg b/doc/docs/figure/dependency-limitations.svg new file mode 100644 index 0000000..329bd61 --- /dev/null +++ b/doc/docs/figure/dependency-limitations.svg @@ -0,0 +1,616 @@ + + + + + + image/svg+xml + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/doc/docs/figure/dependency-map-resolver.svg b/doc/docs/figure/dependency-map-resolver.svg new file mode 100644 index 0000000..aa75930 --- /dev/null +++ b/doc/docs/figure/dependency-map-resolver.svg @@ -0,0 +1,316 @@ + + + + + + image/svg+xml + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/doc/docs/figure/dependency-sink.svg b/doc/docs/figure/dependency-sink.svg new file mode 100644 index 0000000..a663a88 --- /dev/null +++ b/doc/docs/figure/dependency-sink.svg @@ -0,0 +1,196 @@ + + + + + + image/svg+xml + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/doc/docs/figure/dependency-source.svg b/doc/docs/figure/dependency-source.svg new file mode 100644 index 0000000..351bca7 --- /dev/null +++ b/doc/docs/figure/dependency-source.svg @@ -0,0 +1,196 @@ + + + + + + image/svg+xml + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/doc/docs/lang/signal.md b/doc/docs/lang/signal.md index 2a7abca..6942690 100644 --- a/doc/docs/lang/signal.md +++ b/doc/docs/lang/signal.md @@ -4,7 +4,7 @@ Signal is a collection of types that can be transferred through wires in HazardF The HazardFlow HDL reuse some data types from the Rust programming language. Normally we can consider a data type implements [`Copy` trait in Rust](https://doc.rust-lang.org/std/marker/trait.Copy.html) as a signal type in the HazardFlow HDL. -> The `Copy` trait in Rust and the signal type in HazardFlow are not in a perfect 1:1 relationship. +> NOTE: The `Copy` trait in Rust and the signal type in HazardFlow are not in a perfect 1:1 relationship. While the signal type in HazardFlow must implement Rust's `Copy` trait, there are some types like function pointers (e.g., `fn() -> i32`) that implement the `Copy` trait but are not treated as signal types in HazardFlow. For more information of the Rust data types, please refer to [The Rust Programming Language Book](https://doc.rust-lang.org/beta/book/ch03-02-data-types.html).