xls icon indicating copy to clipboard operation
xls copied to clipboard

[enhancement] Add procs for monitoring channels in DSLX

Open rw1nkler opened this issue 9 months ago • 0 comments

What's hard to do? (limit 100 words)

In DSLX, there is currently no way to verify data sent over channels without actually receiving it. This limitation requires modifying the design for integration tests, involving multiple processes, to verify data flow. This can be done either by receiving the data within the test proc and manually sending it to the next proc or by adding additional procs to the design to verify and forward the data.

However, even if you modify the design to receive, check, and resend the data, you still can't confirm if the target process consumed the data correctly. As a result, the final checks may not accurately reflect the system's actual behavior.

Current best alternative workaround (limit 100 words)

One can check the results of the --trace_channels option to verify the system's behavior, but there is no mechanism in the DSLX language to perform this verification directly.

Your view of the "best case XLS enhancement" (limit 100 words)

DSLX could have a special monitor proc, capable of validating the data associated with one end of the channel. When connected to the out channel it could receive a copy of data sent on the channel; for the in channels it could get a copy of data consumed by the target proc. This will allow for validating both sides of the communication from the DSLX language.

The syntax for the monitor proc may be the same as the normal proc, but it could be marked with an additional #[monitor] attribute. If passing the same channel to multiple procs is not an option (although it is possible now in test procs) or a slightly different meaning of channels passed to the monitor proc is not wanted, an additional built-in may be considered. This built-in would take a normal channel and return a monitored channel that can be passed only to monitor-like procs.

The main point of this idea is to feed the monitor proc with the actual data send to/received from the channel. Because of that the data received by the monitor should come from the add/pop callbacks from the channel queue.

The snippet bellow shows a possible usage of a monitor proc:

import std;

// Definitions of IncreamentalGenerator, Multiply, Add and Flog2 procs
// ...

#[monitor]
proc MonotonicityMonitor {
  data_r: mon_chan<u32> in;

  init { u32:0 }

  config(data_r: chan<u32> in) {
    (data_r,)
  }

  next(prev: u32) {
    // Monitor verifying if the data is correct, either by comparing it to a list of 
    // the expected values, or by checking some of the properties that the data should have
    let (tok, data) = recv(join(), data_r);
    assert!(data >= prev, "Data value is decreasing");

    data
  }
}

const EXPECTED_DATA = u32[10]:[ u32:1, u32:2, u32:3, u32:3, u32:4, u32:4, u32:4, u32:4, u32:5, u32:5];

#[test_proc]
proc test_proc {
    terminator: chan<bool> out;
    data_r: chan<u32> in;

    config(terminator: chan<bool> out) {
        let (data0_s, data0_r) = chan<u32>("data0");
        let (data1_s, data1_r) = chan<u32>("data1");
        let (data2_s, data2_r) = chan<u32>("data2");
        let (data3_s, data3_r) = chan<u32>("data3");

        // The tested design
        spawn IncrementalGenerator(data0_s);
        spawn Multiply<u32:2>(data0_r, data1_s);
        spawn Flog2(data1_r, data2_s);
        spawn Add<u32:1>(data2_r, data3_s);

        // Monitors that can be added without any modifications of the design above
        let data1_s_mon = monitor(data_1_s);
        spawn MonotonicityMonitor(data1_s_mon);

        (terminator, data3_r)
    }

    init { () }

    next(state: ()) {
        // Tests checking the expected behavior of the entire system
        let tok = for (exp_data, tok): (u32, token) in EXPECTED_DATA {
            let (tok, data) = recv(tok, data_r);
            trace_fmt!("Received: {} ?= {}", data, exp_data);
            assert_eq(data, exp_data);
            (tok)
        }(join());

        send(tok, terminator, true);
    }
}

rw1nkler avatar May 28 '24 14:05 rw1nkler