From aa88e65c3d92811702a684998f9b6fb5b04912c1 2020-02-10 15:15:28 From: Christopher Esterhuyse Date: 2020-02-10 15:15:28 Subject: [PATCH] exchange --- diff --git a/src/runtime/actors.rs b/src/runtime/actors.rs index 157a440160a6049f915af2342f58892b125d799d..f43bf2ce7f3d8dad914a1af7dffddfb9e4a36143 100644 --- a/src/runtime/actors.rs +++ b/src/runtime/actors.rs @@ -381,20 +381,29 @@ impl PolyN { pub fn become_mono( mut self, + logger: &mut String, decision: &Predicate, table_row: &mut HashMap, ) -> MonoN { - if let Some((_, branch)) = self + log!( + logger, + "decision {:?} with branch preds {:?}", + decision, + self.branches.iter().collect::>() + ); + if let Some((branch_pred, branch)) = self .branches .drain() .find(|(p, branch)| branch.to_get.is_empty() && decision.satisfies(p)) { + log!(logger, "decision {:?} mapped to branch {:?}", decision, branch_pred); let BranchN { gotten, sync_batch_index, .. } = branch; for (&key, payload) in gotten.iter() { assert!(table_row.insert(key, payload.clone()).is_none()); } MonoN { ekeys: self.ekeys, result: Some((sync_batch_index, gotten)) } } else { + log!(logger, "decision {:?} HAD NO SOLUTION!!?", decision); panic!("No such solution!") } } diff --git a/src/runtime/communication.rs b/src/runtime/communication.rs index eeb6ea42b09ed0cf448c92ae3ae9ac458a31528f..81b9d1b3a649aeae390688ec05ae089980077787 100644 --- a/src/runtime/communication.rs +++ b/src/runtime/communication.rs @@ -6,11 +6,10 @@ impl Controller { log!(&mut self.inner.logger, "ENDING ROUND WITH DECISION! {:?}", &decision); let mut table_row = HashMap::::default(); // 1. become_mono for Poly actors - self.inner.mono_n = self - .ephemeral - .poly_n - .take() - .map(|poly_n| poly_n.become_mono(&decision, &mut table_row)); + self.inner.mono_n = + self.ephemeral.poly_n.take().map(|poly_n| { + poly_n.become_mono(&mut self.inner.logger, &decision, &mut table_row) + }); self.inner.mono_ps.extend( self.ephemeral.poly_ps.drain(..).map(|m| m.become_mono(&decision, &mut table_row)), ); @@ -124,7 +123,7 @@ impl Controller { } log!( &mut self.inner.logger, - "... Initial native branch (batch index={} with pred {:?}", + "... Initial native branch batch index={} with pred {:?}", sync_batch_index, &predicate ); diff --git a/src/runtime/mod.rs b/src/runtime/mod.rs index 9916289f2e3a4cee65066324688a763eeeba31a8..b67ca1439c34d04faf9a69f230f6cd8240d9ff7f 100644 --- a/src/runtime/mod.rs +++ b/src/runtime/mod.rs @@ -386,7 +386,7 @@ impl Predicate { s = s_it.next(); } else if sid > oid { // s is missing this element - o_not_s.push((sid, sb)); + o_not_s.push((oid, ob)); o = o_it.next(); } else if sb != ob { assert_eq!(sid, oid); @@ -408,11 +408,11 @@ impl Predicate { [false, false] => { // ... which is the union of the predicates' assignments but // is equivalent to neither self nor other. - let mut predicate = self.clone(); + let mut new = self.clone(); for (&id, &b) in o_not_s { - predicate.assigned.insert(id, b); + new.assigned.insert(id, b); } - New(predicate) + New(new) } } } diff --git a/src/test/connector.rs b/src/test/connector.rs index d08a7c52d0b49f5879f2a1148f11cc8ab05f0e1d..6445e15cbfded6634b23f9662347d0fc63fabdec 100644 --- a/src/test/connector.rs +++ b/src/test/connector.rs @@ -41,9 +41,14 @@ composite sync_2(in i, out o) { new sync(i, x); new sync(y, o); } -composite forward_pair(in ia, out oa, in ib, out ob) { - new forward(ia, oa); - new forward(ib, ob); +primitive exchange(in ai, out ao, in bi, out bo) { + // Note the implicit causal relationship + while(true) synchronous { + if(fires(ai)) { + put(bo, get(ai)); + put(ao, get(bi)); + } + } } primitive forward_nonzero(in i, out o) { while(true) synchronous { @@ -518,7 +523,6 @@ fn alternator_2() { } #[test] -// PANIC TODO: eval::1536 fn composite_chain_a() { // Check if composition works. Forward messages through long chains /* @@ -558,7 +562,6 @@ fn composite_chain_a() { } #[test] -// PANIC TODO: eval::1536 fn composite_chain_b() { // Check if composition works. Forward messages through long chains /* @@ -598,12 +601,11 @@ fn composite_chain_b() { } #[test] -// PANIC TODO: eval::1605 fn exchange() { /* - /-->forward-->P|A-->forward-->\ - Alice Bob - \<--forward<--P|A<--forward<--/ + /-->\ /-->P|A-->\ /-->\ + Alice exchange exchange Bob + \<--/ \<--P|A<--/ \<--/ */ let timeout = Duration::from_millis(1_500); let addrs = [next_addr(), next_addr()]; @@ -612,39 +614,38 @@ fn exchange() { // &|x| { // Alice - x.configure(PDL, b"forward_pair").unwrap(); + x.configure(PDL, b"exchange").unwrap(); x.bind_port(0, Native).unwrap(); // native in - x.bind_port(1, Passive(addrs[0])).unwrap(); // peer out - x.bind_port(2, Passive(addrs[1])).unwrap(); // peer in - x.bind_port(3, Native).unwrap(); // native out + x.bind_port(1, Native).unwrap(); // native out + x.bind_port(2, Passive(addrs[0])).unwrap(); // peer out + x.bind_port(3, Passive(addrs[1])).unwrap(); // peer in x.connect(timeout).unwrap(); for _ in 0..N { - x.put(0, b"A->B".to_vec()).unwrap(); - x.get(1).unwrap(); + assert_eq!(Ok(()), x.put(0, b"A->B".to_vec())); + assert_eq!(Ok(()), x.get(1)); assert_eq!(Ok(0), x.sync(timeout)); - assert_eq!(Ok(b"B->A" as &[u8]), x.read_gotten(0)); + assert_eq!(Ok(b"B->A" as &[u8]), x.read_gotten(1)); } }, &|x| { // Bob - x.configure(PDL, b"forward_pair").unwrap(); + x.configure(PDL, b"exchange").unwrap(); x.bind_port(0, Native).unwrap(); // native in - x.bind_port(1, Active(addrs[1])).unwrap(); // peer out - x.bind_port(2, Active(addrs[0])).unwrap(); // peer in - x.bind_port(3, Native).unwrap(); // native out + x.bind_port(1, Native).unwrap(); // native out + x.bind_port(2, Active(addrs[1])).unwrap(); // peer out + x.bind_port(3, Active(addrs[0])).unwrap(); // peer in x.connect(timeout).unwrap(); for _ in 0..N { - x.put(0, b"B->A".to_vec()).unwrap(); - x.get(1).unwrap(); + assert_eq!(Ok(()), x.put(0, b"B->A".to_vec())); + assert_eq!(Ok(()), x.get(1)); assert_eq!(Ok(0), x.sync(timeout)); - assert_eq!(Ok(b"A->B" as &[u8]), x.read_gotten(0)); + assert_eq!(Ok(b"A->B" as &[u8]), x.read_gotten(1)); } }, ])); } #[test] -// THIS DOES NOT YET WORK. TODOS are hit fn filter_messages() { // Make a protocol whose behavior depends on the contents of messages // Getter prohibits the receipt of messages of the form [0, ...].