Page 1 of 1

Algorithm needed for Type-System-like Tool

Posted: Tue Nov 15, 2011 1:37 am UTC
by Meteorswarm
I'm working on a formalization of the Concurrent Hardware Process language for describing, well, concurrent hardware systems under the quasi-delay-insensitive model. It's cool, and neat, and we have a problem.

The language provides a notion of communication channels; these are synchronous channels like those in pi calculus, except that they're not first-order, and are all fixed at compile time. Unlike pi calculus, we have to deal with real hardware, and that's where the problem comes in.

Each channel has only two endpoints, and we have a static analysis that enforces that. One endpoint can read from the channel, and one endpoint can write to the channel. Additionally, each endpoint is either passive or active, and each channel must consist of one active and one passive endpoint.

If this were it, we could just arbitrarily assign polarities to the channels, but we have two more features of the language that get in the way:

Probes. You can ask "is this channel waiting to send something?" and "is this channel waiting to receive something?" But, you can only ask these questions if the sending side or the receiving side, respectively, has an active polarity.

Bullets. You can wait for multiple channel actions to occur at once, but all but one of the actions you wait on must involve the passive end of a channel.

I'm really not sure how to solve this. I've been thinking about using a constraints-based approach, but I can't think of a clever way to solve the all-but-one issue that isn't exponential on the number of channels. I could just come up with a bunch of boolean logic statements, and plug them into a constraint solver, but that's not efficient. I'm OK with it being exponential on the number of channels in a bullet, although not exponential is better, of course. I really can't have it be exponential on the size of the program, though.

Is there a better way to infer the channel polarities?

Re: Algorithm needed for Type-System-like Tool

Posted: Tue Nov 15, 2011 3:07 am UTC
by Yakk
Is it a "must" on the single active channel when waiting? Because reducing one-of-three SAT to the polarity assignment problem in this language if you have a "must" is pretty easy. (unless, and it is quite likely, I misread you).

Without a must, hmm. Dunno yet.

With a must, that reduction says you are screwed for the general case. You could still hope for efficient / reasonably good "typical" cases -- ie, a good heuristic algorithm.

Re: Algorithm needed for Type-System-like Tool

Posted: Tue Nov 15, 2011 4:09 am UTC
by Meteorswarm
Yakk wrote:Is it a "must" on the single active channel when waiting? Because reducing one-of-three SAT to the polarity assignment problem in this language if you have a "must" is pretty easy. (unless, and it is quite likely, I misread you).

Without a must, hmm. Dunno yet.

With a must, that reduction says you are screwed for the general case. You could still hope for efficient / reasonably good "typical" cases -- ie, a good heuristic algorithm.


I'm not sure what you mean by "must," so I'll try to explain again and hope I answer the question: when you have multiple simultaneous actions, they can either all be passive, or all but one be passive.

I'm thinking that for a first-pass, I'll just go with making them all passive, which makes this a lot simpler, but I'd really like to do it the fully sophisticated way.

Re: Algorithm needed for Type-System-like Tool

Posted: Tue Nov 15, 2011 10:01 am UTC
by jareds
This looks like it can be reduced to 2SAT, provided I understand your constraints correctly.

Let each endpoint be represented by a boolean variable which is true iff the endpoint is active. You have three types of constraints:

1. Each channel consists of one active and one passive endpoint. Let x and y be endpoints of a channel. This constraint is equivalent to ((x or y) and (not x or not y)).

2. Probes. This just forces some endpoint x to be active, and is thus equivalent to the term x (which to be pedantic is equivalent to the disjunct (x or x)).

3. Bullets. Each bullet forces some set of endpoints to have at most one active endpoint. Let S be the set of endpoints of a bullet. This constraint is equivalent to the conjunction, for all pairs of endpoints x and y in S (where x != y), of (not x or not y). For example, if a bullet has endpoints x, y, and z, the constraint is equivalent to ((not x or not y) and (not x or not z) and (not y or not z)).

Since each constraint is equivalent to a 2-CNF formula, the conjunction of all the constraints is equivalent to a 2-CNF formula. The formula will be quadratic in the size of the original constraints (due to bullets), but 2SAT can be solved in linear time, so you should be able to solve your problem in quadratic time. There's a pretty solid description of how to solve 2SAT on Wikipedia, among other places.

Re: Algorithm needed for Type-System-like Tool

Posted: Tue Nov 15, 2011 3:00 pm UTC
by Yakk
jareds wrote:This looks like it can be reduced to 2SAT, provided I understand your constraints correctly.

Let each endpoint be represented by a boolean variable which is true iff the endpoint is active.

Really, each channel should be a boolean variable. One end of the channel is the true end, the other is the false end. The end of the channel that is active is the value of the variable.

Simpler.
You have three types of constraints:

1. Each channel consists of one active and one passive endpoint. Let x and y be endpoints of a channel. This constraint is equivalent to ((x or y) and (not x or not y)).

Aka, x!=y, or x xor y.
2. Probes. This just forces some endpoint x to be active, and is thus equivalent to the term x (which to be pedantic is equivalent to the disjunct (x or x)).

Well, really, this just lets you simplify the problem -- replace x with true.
3. Bullets. Each bullet forces some set of endpoints to have at most one active endpoint. Let S be the set of endpoints of a bullet. This constraint is equivalent to the conjunction, for all pairs of endpoints x and y in S (where x != y), of (not x or not y). For example, if a bullet has endpoints x, y, and z, the constraint is equivalent to ((not x or not y) and (not x or not z) and (not y or not z)).

There are n choose 2 such, or (n)(n-1)/2 such.

... which, as you noted is only quadratic. Damn it, I got about this far, but thought "that'll blow up" without actually thinking that it was only n choose 2. Sigh.

Re: Algorithm needed for Type-System-like Tool

Posted: Tue Nov 15, 2011 11:35 pm UTC
by Meteorswarm
Ah, somehow I hadn't realized 2-sat is cheap, and that I had 2-sat on my hands. That'll do it!

Thanks so much. Now I just need to find (or write myself) a 2-sat solver for ocaml.