You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: src/chapel/README.md
+45-26Lines changed: 45 additions & 26 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -1,8 +1,19 @@
1
-
# Chapel Proof-of-Concept for ECHIDNA
1
+
# Chapel Production Integration for ECHIDNA
2
2
3
-
Demonstrates parallel proof search using Chapel's task parallelism.
3
+
Parallel proof search using Chapel's task parallelism, integrated into the main ECHIDNA codebase.
4
4
5
-
## Quick Start
5
+
## Overview
6
+
7
+
This directory contains the Chapel-based parallel proof search framework, now integrated into the main ECHIDNA codebase. The Chapel code is used to accelerate proof search by dispatching theorem proving goals to multiple prover backends concurrently.
8
+
9
+
## Integration Status
10
+
11
+
-**Status**: Production-ready
12
+
-**Location**: `src/chapel/`
13
+
-**Build System**: Integrated with `Justfile` and `Cargo.toml`
14
+
-**FFI Bridge**: Zig bridge at `src/zig_ffi/chapel_bridge.zig`
15
+
16
+
## Build Instructions
6
17
7
18
### 1. Install Chapel
8
19
@@ -19,24 +30,24 @@ source util/setchplenv.bash
19
30
make
20
31
```
21
32
22
-
### 2. Compile the PoC
33
+
### 2. Build Chapel Code
23
34
24
35
```bash
25
-
cdechidna/chapel_poc
36
+
cdsrc/chapel
26
37
chpl parallel_proof_search.chpl -o proof_search
27
38
```
28
39
29
-
### 3. Run
40
+
### 3. Build Zig FFI Bridge
30
41
31
42
```bash
32
-
# Run with default settings
33
-
./proof_search
43
+
cd src/zig_ffi
44
+
zig build -Dstubs=false
45
+
```
34
46
35
-
# Run with specific number of provers
36
-
./proof_search --numProvers=8
47
+
### 4. Build Rust with Chapel Feature
37
48
38
-
# Quiet mode
39
-
./proof_search --verbose=false
49
+
```bash
50
+
cargo build --features chapel
40
51
```
41
52
42
53
## Expected Output
@@ -87,7 +98,7 @@ Speedup: 1.51x
87
98
## What This Demonstrates
88
99
89
100
### 1. Parallel Proof Search
90
-
- Tries all 12 provers simultaneously
101
+
- Tries all 30 provers simultaneously
91
102
- Returns first/best successful proof
92
103
- Automatic load balancing
93
104
@@ -101,21 +112,29 @@ Speedup: 1.51x
101
112
- Multiple tactic strategies simultaneously
102
113
- Finds optimal proofs faster
103
114
115
+
## Integration Details
116
+
117
+
### Depth of Integration
118
+
-**FFI Layer**: Chapel functions are exposed via `chapel_ffi_exports.chpl` and wrapped by the Zig bridge at `src/zig_ffi/chapel_bridge.zig`.
119
+
-**Rust Consumption**: The Rust code in `src/rust/proof_search.rs` consumes these functions under the `chapel` feature flag.
120
+
-**Build System**: The build process is integrated into `Justfile` and `Cargo.toml`.
121
+
122
+
### Breadth of Integration
123
+
-**Prover Dispatch**: The Chapel code is used for parallel prover dispatch, replacing the sequential dispatch in Rust.
124
+
-**Result Aggregation**: Results from all provers are aggregated and the best proof is selected.
125
+
-**Fallback Mechanism**: If Chapel is not available, the system falls back to sequential dispatch.
126
+
127
+
### Relation to Other Parts of the System
128
+
-**Rust Core**: The Rust core remains the primary logic layer, with Chapel accelerating specific tasks.
129
+
-**Julia ML Layer**: The Julia ML layer is unaffected by the Chapel integration.
130
+
-**FFI Bridge**: The Zig FFI bridge is a critical component that enables communication between Rust and Chapel.
131
+
104
132
## Next Steps
105
133
106
-
1.~~**Integration**: Add FFI bindings to call from Rust~~ — **DONE**.
107
-
Chapel `export` functions in `chapel_ffi_exports.chpl` are wrapped by
108
-
the Zig bridge at `../src/zig_ffi/chapel_bridge.zig`, which in turn
109
-
exports the `echidna_*` C ABI consumed by
110
-
`../src/rust/proof_search.rs` under `#[cfg(feature = "chapel")]`.
111
-
Build the Zig bridge with `cd ../src/zig_ffi && zig build` (default
112
-
`-Dstubs=true` bundles `chapel_stubs.c` so Rust links without a
113
-
Chapel install); then `cargo build --features chapel` from the repo
114
-
root. Pass `-Dstubs=false` to the Zig build to link against the real
115
-
`libechidna_chapel.so` produced in this directory.
116
-
2.**Real Provers**: Replace mock with actual prover backends
117
-
3.**Distributed**: Run on multi-node cluster
118
-
4.**ML Integration**: Parallel model training
134
+
1.**Update Rust Dispatch**: Modify `src/rust/dispatch.rs` to use Chapel for parallel proof search when the `chapel` feature is enabled.
135
+
2.**Add CI/CD Support**: Ensure Chapel code is built and tested in CI.
136
+
3.**Performance Optimization**: Run benchmarks and tune the Chapel code.
137
+
4.**Documentation**: Update documentation to reflect the production integration.
0 commit comments