souffle-lang / souffle

Soufflé is a variant of Datalog for tool designers crafting analyses in Horn clauses. Soufflé synthesizes a native parallel C++ program from a logic specification.
http://souffle-lang.github.io/
Universal Permissive License v1.0
927 stars 208 forks source link

Architecture and Build #150

Closed scyptnex closed 5 years ago

scyptnex commented 8 years ago

(this is a fairly far-away goal)

It seems that souffle execution can be broken into fairly well-defined stages:

  1. Pre-processing (wave)
  2. Parsing
  3. AST to RAM
  4. RAM optimisations
  5. code gen
  6. either:
    1. compiling
    2. interpreting

Personally I need parts of the souffle system without the whole thing, and to do that it needs better interfaces between separate modules in the system. This is standard practice in modern applications, if you need to sell someone on it just say microservices

As a side note, and much more feasible, updating the build system to something like cmake should be done soonish:

@psubotic , bernhard mentioned your team has some architectural requirements. Please tell me if the above is good/bad for what you need. As i understand you also want a different interface to souffle than the command-line executable.

psubotic commented 8 years ago

Hi Nic,

I'm currently working on a basic interface that I need in a hurry. Perhaps this can grow into something which is close to your description.

For a basic interface something like the following is ok for me now:

Compile: AST describing rules x Config env => Execute object

Execute object is an abstract class that describes either a Ram program or a shared C++ library

Execute (Relational Data x Execute Object => Results

Results is a data structure describing the output

You idea is more fine grained. In general I agree with this kind of interface so perhaps this interface im describing can be built on top of a "micro" interface. Thing is, I have to get this done fast so im just going with what I need of now.

On Mon, Jun 20, 2016 at 5:59 PM, Nic H notifications@github.com wrote:

(this is a fairly far-away goal)

It seems that souffle execution can be broken into fairly well-defined stages:

  1. Pre-processing (wave)
  2. Parsing
  3. AST to RAM
  4. RAM optimisations
  5. code gen
  6. either:
    1. compiling
    2. interpreting

Personally I need parts of the souffle system without the whole thing, and to do that it needs better interfaces between separate modules in the system. This is standard practice in modern applications, if you need to sell someone on it just say microservices

As a side note, and much more feasible, updating the build system to something like cmake should be done soonish:

  • platform independence
  • modular build system facilitates modular re-use of the above architecture

@psubotic https://github.com/psubotic , bernhard mentioned your team has some architectural requirements. Please tell me if the above is good/bad for what you need. As i understand you also want a different interface to souffle than the command-line executable.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/souffle-lang/souffle/issues/150, or mute the thread https://github.com/notifications/unsubscribe/AAW3OdaJIbR55AAyzq0GBmZx2ETm3BgUks5qNzd_gaJpZM4I6ROB .

psubotic commented 8 years ago

@herbert I'd be very interested to hear your opinion/input on this

On Mon, Jun 20, 2016 at 6:23 PM, P Subotic psubotic@gmail.com wrote:

Hi Nic,

I'm currently working on a basic interface that I need in a hurry. Perhaps this can grow into something which is close to your description.

For a basic interface something like the following is ok for me now:

Compile: AST describing rules x Config env => Execute object

Execute object is an abstract class that describes either a Ram program or a shared C++ library

Execute (Relational Data x Execute Object => Results

Results is a data structure describing the output

You idea is more fine grained. In general I agree with this kind of interface so perhaps this interface im describing can be built on top of a "micro" interface. Thing is, I have to get this done fast so im just going with what I need of now.

On Mon, Jun 20, 2016 at 5:59 PM, Nic H notifications@github.com wrote:

(this is a fairly far-away goal)

It seems that souffle execution can be broken into fairly well-defined stages:

  1. Pre-processing (wave)
  2. Parsing
  3. AST to RAM
  4. RAM optimisations
  5. code gen
  6. either:
    1. compiling
    2. interpreting

Personally I need parts of the souffle system without the whole thing, and to do that it needs better interfaces between separate modules in the system. This is standard practice in modern applications, if you need to sell someone on it just say microservices

As a side note, and much more feasible, updating the build system to something like cmake should be done soonish:

  • platform independence
  • modular build system facilitates modular re-use of the above architecture

@psubotic https://github.com/psubotic , bernhard mentioned your team has some architectural requirements. Please tell me if the above is good/bad for what you need. As i understand you also want a different interface to souffle than the command-line executable.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/souffle-lang/souffle/issues/150, or mute the thread https://github.com/notifications/unsubscribe/AAW3OdaJIbR55AAyzq0GBmZx2ETm3BgUks5qNzd_gaJpZM4I6ROB .

b-scholz commented 8 years ago

We have already a C++ interface for generated C++ classes. Perhaps we can replicate some of the details for this more general interface. The issue we always have is how to deal with symbols and integer numbers at the same time in a tuple. The problem is that we work with symbol tables and symbols are stored as numbers in memory. This needs to be taken into account.

We also need an extra mode for the compilation, i.e., generating a shared library. The compile scripts would need to be changed (souffle-compile.in), and we need an extra option and an extra information in the configuration environment.

HerbertJordan commented 8 years ago

I was always in favor of cmake, but right now I'd say never touch a running system. If it works, don't spend the effort in changing it until we have a problem that can be easier solved using cmake.

For the architecture cleanup, we should start listing the actual use case scenarios the clients would like to use souffle in -- not proposed solutions derived out of those. We need to understand the need behind those requests.

The current standard use-case at the moment is to use souffle similar to bison, to generate a code file covering an analysis (in comparison to a parser produced by bison) which can be included in a C/C++ project build.

In this case, only the interface to the produced analysis as well as the parameters of the souffle command line tool are important. All the rest is hidden from the user and we can change it freely.

Please, list alternative use cases you would like to support in this thread.

psubotic commented 8 years ago

My opinion is the following: Datalog and Horn clauses in general are becoming a popular IR for verification engines. Like SMT solvers, the usual use case is increasingly becoming: have a domain specific problem - convert it to a logic representation (SAT, SMT, Datalog) and use an off the shelf solver to compute a solution. This is precisely the scenario I have (cannot give details for obvious reasons). A tool may want to integrate with Souffle like it integrates with Z3 - they build up a set of formulae via a data structure and send it off to the solver and get a result in a specific format. If they want to use options like compile etc they just set the flag. I actually think this is the standard use case and not the bison one, although I do not disagree that the bison use case is also very important.

HerbertJordan commented 8 years ago

To efficiently support the use case described by @psubotic we would have to provide a nice, clean version of the AST so that we can actually allow an external user to see and use it directly. This is quite some effort.

Alternatively, I would recommend for Paul's use case to use strings as an interface. The clients formulate their rules by writing them into a string buffer and then use the parser to run the query (as, for instance, done by the unit tests). What we would have to add there is a way to get the results -- without the need of reading them from a file.

Or, we really read them from the resulting fact file and call this the "user interface" (no-effort).

psubotic commented 8 years ago

For now im using the AST - its not as bad as I though but I agree with Herbert -- a user friendly version would be nice with operator overloading, builder pattern etc. to make it EDSL-ike.

The sting idea was rejected by the users.

I'll finish up with the AST and ill keep it separate from the Souffle mainline. We can have a look at it and plan how to integrate it into souffle. I'm happy to put in the hard work. We will automatically get a java/scala interface (im doing this too) would be also nice to support some more languages like python, ocaml, .net. Im happy to also do the ocaml one but I really know nothing about python and .net

I suggest we all have a skype once I get what im doing finished (say after CAV).

On Mon, Jun 27, 2016 at 2:59 PM, Herbert Jordan notifications@github.com wrote:

To efficiently support the use case described by @psubotic https://github.com/psubotic we would have to provide a nice, clean version of the AST what we can actually allow an external user to see and use. This is quite some effort.

Alternatively, I would recommend for Paul's use case to use strings as an interface. The clients formulate their rules by writing them into a string buffer and then use the parser to run the query (as, for instance, done by the unit tests). What we would have to add there is a way to get the results -- without the need of reading them from a file.

Or, we really read them from the resulting fact file and call this the "user interface".

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/souffle-lang/souffle/issues/150#issuecomment-228888828, or mute the thread https://github.com/notifications/unsubscribe/AAW3ORXop8WcMN0DKmZ7VTF_4zuB7WN1ks5qQEfLgaJpZM4I6ROB .