weirflow 0.1.0

GPU-first dataflow analysis primitives for Vyre and Santh compiler pipelines.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77

//! Property-based gates for `weir::slice::backward_slice` Program
//! construction.
//!
//! Op id: `weir::tests::df::property::slice_construction`.
//! Soundness: `MayOver`. Properties exercised: per-call name
//! independence, idempotent construction (equal shape+name → same
//! buffer set), and frontier-buffer presence across random shapes.

use proptest::prelude::*;
use vyre_primitives::graph::program_graph::ProgramGraphShape;
use weir::slice::backward_slice;

fn name(prefix: &str, salt: u32) -> String {
    format!("{prefix}_{salt}")
}

proptest! {
    #![proptest_config(ProptestConfig::with_cases(10_000))]

    /// Every construction emits frontier_in + frontier_out under
    /// the requested names.
    #[test]
    fn frontier_buffers_use_requested_names(
        nodes in 1u32..256,
        edges in 1u32..256,
        salt in any::<u32>(),
    ) {
        let shape = ProgramGraphShape::new(nodes, edges);
        let fin_n = name("fin", salt);
        let fout_n = name("fout", salt);
        let prog = backward_slice(shape, &fin_n, &fout_n);
        let names: Vec<&str> = prog.buffers().iter().map(|b| b.name()).collect();
        prop_assert!(names.contains(&fin_n.as_str()));
        prop_assert!(names.contains(&fout_n.as_str()));
    }

    /// Equal shape + names must produce equal buffer name set
    /// (deterministic construction).
    #[test]
    fn deterministic_construction(
        nodes in 1u32..256,
        edges in 1u32..256,
        salt in any::<u32>(),
    ) {
        let shape = ProgramGraphShape::new(nodes, edges);
        let fin_n = name("fin", salt);
        let fout_n = name("fout", salt);
        let a = backward_slice(shape, &fin_n, &fout_n);
        let b = backward_slice(shape, &fin_n, &fout_n);
        let names_a: Vec<&str> = a.buffers().iter().map(|x| x.name()).collect();
        let names_b: Vec<&str> = b.buffers().iter().map(|x| x.name()).collect();
        prop_assert_eq!(names_a, names_b);
    }

    /// Different names produce disjoint buffer sets in the renamed
    /// frontiers.
    #[test]
    fn names_are_independent(
        nodes in 1u32..256,
        edges in 1u32..256,
        salt_a in any::<u32>(),
        salt_b in any::<u32>(),
    ) {
        prop_assume!(salt_a != salt_b);
        let shape = ProgramGraphShape::new(nodes, edges);
        let a_in = name("fin", salt_a);
        let a_out = name("fout", salt_a);
        let b_in = name("fin", salt_b);
        let b_out = name("fout", salt_b);
        let a = backward_slice(shape, &a_in, &a_out);
        let b = backward_slice(shape, &b_in, &b_out);
        let names_a: Vec<&str> = a.buffers().iter().map(|x| x.name()).collect();
        let names_b: Vec<&str> = b.buffers().iter().map(|x| x.name()).collect();
        prop_assert!(names_a.contains(&a_in.as_str()) && !names_a.contains(&b_in.as_str()));
        prop_assert!(names_b.contains(&b_in.as_str()) && !names_b.contains(&a_in.as_str()));
    }
}