search

bloom-lang / bud

Prototype Bud runtime (Bloom Under Development)
http://bloom-lang.net
Other
854 stars 60 forks source link

Tool support for CALM analysis #253

Open neilconway opened 12 years ago

neilconway commented 12 years ago

We don't actually have a programmatic way to check if a program satisfies the CALM analysis (other than "stare at the budplot output looking for ..."). It would be nice to provide some simple analysis tools to do this automatically.

sriram-srinivasan commented 12 years ago

Can you clarify what kind of analysis is missing? What else can one do besides the conservative check on monotonicity conditions that is already performed?

neilconway commented 12 years ago

Well, we currently have:

  1. analysis for monotonicity as part of program rewriting
  2. system catalogs that can provide programmatic access to this data
  3. budplot viz of program dataflow / monotonicity

It would be nice to have:

  1. A programmatic check for confluence (see the Dedalus paper); this requires stuff like making sure all channel input is persisted into a table
  2. The confluence analysis needs to be made more robust for real-world programs -- e.g., requiring all messages sent over channels to be stored forever is not realistic. (Perhaps this is a separate issue though.)
  3. More generally, tools that enable developers to use confluence/monotonicity as part of the program design process, without requiring them to rerun budplot and stare at diagrams
sriram-srinivasan commented 12 years ago

The dedalus paper mentions confluence once, and leaves it as further work. It is not clear to me how one can prove a system confluent in this setup, when a notion of randomness or choice is part of the primitves. Actually, to take a step back, I need to understand what confluence analysis even means.

It would be nice to have:

  1. A programmatic check for confluence (see the Dedalus paper); this requires stuff like making sure all channel input is persisted into a table

You can't mandate that all channel input is persisted, as in the chat example. One could presumably check if a channel tuple is being read, but even that should not be mandated: "drop all channel inputs until state==READY" is a reasonable requirement.

  1. The confluence analysis needs to be made more robust for real-world programs -- e.g., requiring all messages sent over channels to be stored forever is not realistic. (Perhaps this is a separate issue though.)

yes.

  1. More generally, tools that enable developers to use confluence/monotonicity as part of the program design process, without requiring them to rerun budplot and stare at diagrams

Is it possible to furnish an example of a problem that you have spent considerable time tracking, and would have been nice if it was programmatically analyzed?

neilconway commented 12 years ago

Whoops -- the best place to read about confluence is probably the ICDT submission; I'll send it to you offline.

Re: mandating that channel input is persisted, that is the current requirement (... which was posed in the context of a theory paper). Certainly revisiting that for a practical analysis would be a good idea.

As far as a practical example, I don't really have one, but that would certainly be a good thing to start with.