1
Fork 0

Added liveness analysis for protocols, and removed warnings about empty states.

This commit is contained in:
Eric Holk 2012-07-17 17:03:27 -07:00
parent c858eb0654
commit 7b8171ef2d
10 changed files with 130 additions and 19 deletions

View file

@ -81,7 +81,7 @@ fn from_port<A:send>(-port: future_pipe::client::waiting<A>) -> future<A> {
port_ <-> *port;
let port = option::unwrap(port_);
alt recv(port) {
future_pipe::completed(data, _next) { #move(data) }
future_pipe::completed(data) { #move(data) }
}
}
}
@ -135,10 +135,8 @@ fn with<A,B>(future: future<A>, blk: fn(A) -> B) -> B {
proto! future_pipe {
waiting:recv<T:send> {
completed(T) -> terminated
completed(T) -> !
}
terminated:send { }
}
#[test]

View file

@ -253,6 +253,14 @@ impl methods for bitv {
fn each(f: fn(bool) -> bool) { each(self, f) }
fn each_storage(f: fn(&uint) -> bool) { each_storage(self, f) }
fn eq_vec(v: ~[uint]) -> bool { eq_vec(self, v) }
fn ones(f: fn(uint) -> bool) {
for uint::range(0, self.nbits) |i| {
if self.get(i) {
if !f(i) { break }
}
}
}
}
impl of to_str::to_str for bitv {

View file

@ -27,6 +27,9 @@ fn expand_proto(cx: ext_ctxt, _sp: span, id: ast::ident,
// check for errors
visit(proto, cx);
// do analysis
liveness::analyze(proto, cx);
// compile
base::mr_item(proto.compile(cx))
}

View file

@ -0,0 +1,91 @@
/*
Liveness analysis for protocols. This is useful for a lot of possible
optimizations.
This analysis computes the "co-live" relationship between
states. Co-live is defined inductively as follows.
1. u is co-live with v if u can transition to v in one message.
2. u is co-live with v if there exists a w such that u and w are
co-live, w and v are co-live, and u and w have the same direction.
This relationship approximates when it is safe to store two states in
the same memory location. If there is no u such u is co-live with
itself, then the protocol is bounded.
(These assertions could use proofs)
In addition, this analysis does reachability, to warn when we have
useless states.
The algorithm is a fixpoint computation. For each state, we initialize
a bitvector containing whether it is co-live with each other state. At
first we use rule (1) above to set each vector. Then we iterate
updating the states using rule (2) until there are no changes.
*/
import dvec::extensions;
import std::bitv::{bitv, methods};
import proto::methods;
import ast_builder::empty_span;
fn analyze(proto: protocol, _cx: ext_ctxt) {
#debug("initializing colive analysis");
let num_states = proto.num_states();
let colive = do (copy proto.states).map_to_vec |state| {
let bv = bitv(num_states, false);
for state.reachable |s| {
bv.set(s.id, true);
}
bv
};
let mut i = 0;
let mut changed = true;
while changed {
changed = false;
#debug("colive iteration %?", i);
for colive.eachi |i, this_colive| {
let this = proto.get_state_by_id(i);
for this_colive.ones |j| {
let next = proto.get_state_by_id(j);
if this.dir == next.dir {
changed = changed || this_colive.union(colive[j]);
}
}
}
i += 1;
}
#debug("colive analysis complete");
// Determine if we're bounded
let mut self_live = ~[];
for colive.eachi |i, bv| {
if bv.get(i) {
vec::push(self_live, proto.get_state_by_id(i))
}
}
if self_live.len() > 0 {
let states = str::connect(self_live.map(|s| *s.name), ~" ");
#debug("protocol %s is unbounded due to loops involving: %s",
*proto.name, states);
// Someday this will be configurable with a warning
//cx.span_warn(empty_span(),
// #fmt("protocol %s is unbounded due to loops \
// involving these states: %s",
// *proto.name,
// states));
}
else {
#debug("protocol %s is bounded. yay!", *proto.name);
}
}

View file

@ -55,6 +55,7 @@ impl methods for message {
enum state {
state_(@{
id: uint,
name: ident,
dir: direction,
ty_params: ~[ast::ty_param],
@ -81,6 +82,20 @@ impl methods for state {
cx.ty_path_ast_builder
(path(self.name).add_tys(cx.ty_vars(self.ty_params)))
}
/// Iterate over the states that can be reached in one message
/// from this state.
fn reachable(f: fn(state) -> bool) {
for self.messages.each |m| {
alt m {
message(_, _, _, some({state: id, _})) {
let state = self.proto.get_state(id);
if !f(state) { break }
}
_ { }
}
}
}
}
enum protocol {
@ -104,6 +119,8 @@ impl methods for protocol {
self.states.find(|i| i.name == name).get()
}
fn get_state_by_id(id: uint) -> state { self.states[id] }
fn has_state(name: ident) -> bool {
self.states.find(|i| i.name == name) != none
}
@ -113,6 +130,7 @@ impl methods for protocol {
let messages = dvec();
let state = state_(@{
id: self.states.len(),
name: name,
dir: dir,
ty_params: ty_params,
@ -127,6 +145,8 @@ impl methods for protocol {
fn filename() -> ~str {
~"proto://" + *self.name
}
fn num_states() -> uint { self.states.len() }
}
trait visitor<Tproto, Tstate, Tmessage> {

View file

@ -87,5 +87,6 @@ mod ext {
mod pipec;
mod proto;
mod check;
mod liveness;
}
}

View file

@ -11,16 +11,14 @@ import pipes::{try_recv, recv};
proto! oneshot {
waiting:send {
signal -> signaled
signal -> !
}
signaled:send { }
}
fn main() {
let iotask = uv::global_loop::get();
let c = pipes::spawn_service(oneshot::init, |p| {
pipes::spawn_service(oneshot::init, |p| {
alt try_recv(p) {
some(*) { fail }
none { }
@ -36,8 +34,6 @@ fn main() {
// Make sure the right thing happens during failure.
fn failtest() {
let iotask = uv::global_loop::get();
let (c, p) = oneshot::init();
do task::spawn_with(c) |_c| {

View file

@ -6,10 +6,8 @@ import std::uv;
proto! oneshot {
waiting:send {
signal -> signaled
signal -> !
}
signaled:send { }
}
fn main() {

View file

@ -11,8 +11,6 @@ proto! oneshot {
waiting:send {
signal -> !
}
signaled:send { }
}
proto! stream {

View file

@ -7,10 +7,8 @@ import pipes::recv;
proto! oneshot {
waiting:send {
signal -> signaled
signal -> !
}
signaled:send { }
}
fn main() {
@ -19,7 +17,7 @@ fn main() {
let c = pipes::spawn_service(oneshot::init, |p| { recv(p); });
let iotask = uv::global_loop::get();
sleep(iotask, 5000);
sleep(iotask, 500);
signal(c);
}