Skip to content

Commit

Permalink
Merge pull request #19 from zeskeertwee/threads
Browse files Browse the repository at this point in the history 
Implement threads for proving, working on #18
  • Loading branch information
@alegnani
alegnani authored Jun 11, 2024
2 parents 61b0ce5 + 60f2e4c commit b70168d
Show file tree
Hide file tree
Showing 3 changed files with 134 additions and 33 deletions.
48 changes: 48 additions & 0 deletions verifactory_app/src/async_resource.rs
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,48 @@
use std::thread::{self, JoinHandle};

pub enum AsyncResource<T> {
Pending(Option<JoinHandle<T>>),
Finished(T),
Error(String)
}

impl<T> AsyncResource<T> {
pub fn new<F: FnOnce() -> T>(f: F) -> Self {
Self::Pending(Some(thread::spawn(f)))
}

pub fn poll(&mut self) -> Self {
match self {
AsyncResource::Pending(t) => {
if t.is_finished() {
match t.take().unwrap().join() {
Ok(v) => *self = AsyncResource::Finished(v),
Err(e) => *self = AsyncResource::Error(format!("{:?}", e)),
}
}
},
_ => (),
}
}

pub fn is_pending(&self) -> bool {
match self {
AsyncResource::Pending(_) => true,
_ => false,
}
}

pub fn is_finished(&self) -> bool {
match self {
AsyncResource::Finished(_) => true,
AsyncResource::Error(_) => true,
}
}

pub fn get_result(&self) -> Option<&T> {
match self {
AsyncResource::Finished(t) => Some(t),
_ => None
}
}
}
117 changes: 84 additions & 33 deletions verifactory_app/src/gui/app.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ use verifactory_lib::{
ir::{CoalesceStrength, FlowGraph, FlowGraphFun, Node, Reversable},
utils::Position,
};
use crate::async_resource::AsyncResource;

use super::menu::BlueprintString;

Expand Down Expand Up @@ -77,10 +78,30 @@ impl IOState {

#[derive(Default)]
pub struct ProofState {
balancer: Option<ProofResult>,
equal_drain: Option<ProofResult>,
throughput_unlimited: Option<ProofResult>,
universal: Option<ProofResult>,
balancer: Option<AsyncResource<ProofResult>>,
equal_drain: Option<AsyncResource<ProofResult>>,
throughput_unlimited: Option<AsyncResource<ProofResult>>,
universal: Option<AsyncResource<ProofResult>>,
}

impl ProofState {
pub fn poll_all(&mut self) {
if let Some(v) = &mut self.balancer {
v.poll();
}

if let Some(v) = &mut self.equal_drain {
v.poll();
}

if let Some(v) = &mut self.throughput_unlimited {
v.poll();
}

if let Some(v) = &mut self.universal {
v.poll();
}
}
}

pub type EntityGrid = Vec<Vec<Option<FBEntity<i32>>>>;
Expand Down Expand Up @@ -173,6 +194,8 @@ impl MyApp {

impl eframe::App for MyApp {
fn update(&mut self, ctx: &egui::Context, frame: &mut eframe::Frame) {
self.proof_state = self.proof_state.poll_all();

// Set up toast notifications in the top right
let mut toasts = Toasts::new()
.anchor(Align2::RIGHT_TOP, (-10.0, 10.0))
Expand Down Expand Up @@ -267,29 +290,43 @@ impl eframe::App for MyApp {
// TODO: figure out lifetimes and fix code duplication
ui.heading("Is it a belt-balancer?");
ui.horizontal(|ui| {
if ui.button("Prove").clicked() {
let graph = self.generate_graph(false);
let mut proof = BlueprintProofEntity::new(graph);
let res = proof.model(belt_balancer_f, ModelFlags::empty());
self.proof_state.balancer = Some(res);
if self.proof_state.balancer.is_none() {
if ui.button("Prove").clicked() {
self.proof_state.balancer = Some(AsyncResource::new(|| {
let graph = self.generate_graph(false);
let mut proof = BlueprintProofEntity::new(graph);
proof.model(belt_balancer_f, ModelFlags::empty())
}));
}
}
if let Some(proof_res) = self.proof_state.balancer {
ui.label(format!("Proof result: {}", proof_res));
else if let Some(proof_res) = &self.proof_state.balancer {
if let Some(r) = proof_res.get_result() {
ui.label(format!("Proof result: {}", r));
} else {
ui.label("Pending...");
}
}
});

ui.label("\n");

ui.heading("Is it an equal drain belt-balancer (assumes it is a belt-balancer)?");
ui.horizontal(|ui| {
if ui.button("Prove").clicked() {
let graph = self.generate_graph(true);
let mut proof = BlueprintProofEntity::new(graph);
let res = proof.model(equal_drain_f, ModelFlags::empty());
self.proof_state.equal_drain = Some(res);
if self.proof_state.equal_drain.is_none() {
if ui.button("Prove").clicked() {
self.proof_state.equal_drain = Some(AsyncResource::new(|| {
let graph = self.generate_graph(true);
let mut proof = BlueprintProofEntity::new(graph);
proof.model(equal_drain_f, ModelFlags::empty())
}));
}
}
if let Some(proof_res) = self.proof_state.equal_drain {
ui.label(format!("Proof result: {}", proof_res));
else if let Some(proof_res) = &self.proof_state.equal_drain {
if let Some(r) = proof_res.get_result() {
ui.label(format!("Proof result: {}", r));
} else {
ui.label("Pending...");
}
}
});

Expand All @@ -299,29 +336,43 @@ impl eframe::App for MyApp {
"Is it a throughput unlimited belt-balancer (assumes it is a belt-balancer)?",
);
ui.horizontal(|ui| {
if ui.button("Prove").clicked() {
let graph = self.generate_graph(false);
let mut proof = BlueprintProofEntity::new(graph);
let entities = self.grid.iter().flatten().flatten().cloned().collect();
let res = proof.model(throughput_unlimited(entities), ModelFlags::Relaxed);
self.proof_state.throughput_unlimited = Some(res);
if self.proof_state.throughput_unlimited.is_none() {
if ui.button("Prove").clicked() {
self.proof_state.throughput_unlimited = Some(AsyncResource::new(|| {
let graph = self.generate_graph(false);
let mut proof = BlueprintProofEntity::new(graph);
let entities = self.grid.iter().flatten().flatten().cloned().collect();
proof.model(throughput_unlimited(entities), ModelFlags::Relaxed)
}));
}
}
if let Some(proof_res) = self.proof_state.throughput_unlimited {
ui.label(format!("Proof result: {}", proof_res));
else if let Some(proof_res) = &self.proof_state.throughput_unlimited {
if let Some(r) = proof_res.get_result() {
ui.label(format!("Proof result: {}", r));
} else {
ui.label("Pending...");
}
}
});
ui.label("\n");

ui.heading("Is it a universal belt-balancer?");
ui.horizontal(|ui| {
if ui.button("Prove").clicked() {
let graph = self.generate_graph(false);
let mut proof = BlueprintProofEntity::new(graph);
let res = proof.model(universal_balancer, ModelFlags::Blocked);
self.proof_state.universal = Some(res);
if self.proof_state.universal.is_none() {
if ui.button("Prove").clicked() {
self.proof_state.universal = Some(AsyncResource::new(|| {
let graph = self.generate_graph(false);
let mut proof = BlueprintProofEntity::new(graph);
proof.model(universal_balancer, ModelFlags::Blocked)
}));
}
}
if let Some(proof_res) = self.proof_state.universal {
ui.label(format!("Proof result: {}", proof_res));
else if let Some(proof_res) = &self.proof_state.universal {
if let Some(r) = proof_res.get_result() {
ui.label(format!("Proof result: {}", r));
} else {
ui.label("Pending...");
}
}
});

Expand Down
2 changes: 2 additions & 0 deletions verifactory_app/src/main.rs
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
mod gui;
mod async_resource;

use std::{fs::File, sync::Arc};

use eframe::NativeOptions;
Expand Down

0 comments on commit b70168d

Please sign in to comment.