Hello,

I think I have encountered several cases where Souffle falls into a deadlock and continues executing without producing anything at all. This seems to be independent of the analysis I am running but I can share with you both the analysis code and the facts I'm using. Right now I keep running the same analysis over over with -j 16. It is supposed to run in about 20-22 mins with maximum memory consumed 30GB.

The analysis executable produced sometimes crashes with bad allocation (the error is related to read and write locks) and other times seems to fall into a deadlock, with the memory unchanged for hours and 1600% CPU usage. We used gdb to check where it is stuck and here it is:

$ gdb /home/anantoni/Development/cache/souffle-analyses/fully-guided-context-sensitive/37dc31dec70d2a418f1ec2ddd9512ace022c92f4eb37364dc58ed0d0227818f1 13602GNU gdb (GDB) Fedora 8.0.1-36.fc27 (gdb) bt #0 0x0000000000435984 in souffle::OptimisticReadWriteLock::start_read() () #1 0x00000000005942be in souffle::detail::btree<souffle::ram::Tuple<int, 4ul>, souffle::ram::index_utils::comparator<0u, 1u, 2u, 3u>, std::allocator<souffle::ram::Tuple<int, 4ul> >, 256u, souffle::detail::binary_search, true, souffle::ram::index_utils::comparator<0u, 1u, 2u, 3u>, souffle::detail::updater<souffle::ram::Tuple<int, 4ul> > >::insert(souffle::ram::Tuple<int, 4ul> const&, souffle::detail::btree<souffle::ram::Tuple<int, 4ul>, souffle::ram::index_utils::comparator<0u, 1u, 2u, 3u>, std::allocator<souffle::ram::Tuple<int, 4ul> >, 256u, souffle::detail::binary_search, true, souffle::ram::index_utils::comparator<0u, 1u, 2u, 3u>, souffle::detail::updater<souffle::ram::Tuple<int, 4ul> > >::btree_operation_hints<1u>&) () #2 0x00000000005948f7 in souffle::detail::btree<souffle::ram::Tuple<int, 4ul>, souffle::ram::index_utils::comparator<0u, 1u, 2u, 3u>, std::allocator<souffle::ram::Tuple<int, 4ul> >, 256u, souffle::detail::binary_search, true, souffle::ram::index_utils::comparator<0u, 1u, 2u, 3u>, souffle::detail::updater<souffle::ram::Tuple<int, 4ul> > >::insert(souffle::ram::Tuple<int, 4ul> const&, souffle::detail::btree<souffle::ram::Tuple<int, 4ul>, souffle::ram::index_utils::comparator<0u, 1u, 2u, 3u>, std::allocator<souffle::ram::Tuple<int, 4ul> >, 256u, souffle::detail::binary_search, true, souffle::ram::index_utils::comparator<0u, 1u, 2u, 3u>, souffle::detail::updater<souffle::ram::Tuple<int, 4ul> > >::btree_operation_hints<1u>&) () #3 0x00000000005948f7 in souffle::detail::btree<souffle::ram::Tuple<int, 4ul>, souffle::ram::index_utils::comparator<0u, 1u, 2u, 3u>, std::allocator<souffle::ram::Tuple<int, 4ul> >, 256u, souffle::detail::binary_search, true, souffle::ram::index_utils::comparator<0u, 1u, 2u, 3u>, souffle::detail::updater<souffle::ram::Tuple<int, 4ul> > >::insert(souffle::ram::Tuple<int, 4ul> const&, souffle::detail::btree<souffle::ram::Tuple<int, 4ul>, souffle::ram::index_utils::comparator<0u, 1u, 2u, 3u>, std::allocator<souffle::ram::Tuple<int, 4ul> >, 256u, souffle::detail::binary_search, true, souffle::ram::index_utils::comparator<0u, 1u, 2u, 3u>, souffle::detail::updater<souffle::ram::Tuple<int, 4ul> > >::btree_operation_hints<1u>&) ()

Thanks in advance, Anastasis

Hello, Is there any documentation that tells how to design datalog rules that helps souffle compiler to synthesize parallel evaluator? I wrote a control flow analysis in souffle datalog that has many rules, but unfortunately souffle did not manage to parallelize it enough. I'd like to refactor my code and make it more parallel and faster. My CFA code: https://github.com/grin-compiler/ghc-grin/tree/d7aebb21fd78eda7f86a85868f79d36a071038de/lambda-grin/souffle-datalog

Thanks!

This is a WIP but it's already useful.

If you know cmake, this should be straightforward to use. I will update the README once closer to being finished.

For the uninitiated, see here or just follow the below:

1. cmake >= 3.15 required
2. In your srcdir, run cmake -S . -B <build_dir> or cmake -S . -B <build_dir> -D<option>=<value> if you want to control settings (documented in the root CMakeFile.txt). You can also use ccmake <build_dir> after to see which options are set.
3. The run cmake --build <build_dir> [-j16] and souffle will build
4. To run tests, cd <build_dir>; ctest [-j16] or even just cmake --build <build_dir> [-j16] --target test

I've made sure the compilation flags are the same on Linux 32/64. You can run both cmake and ctest with --verbose to see compile lines or test executions. Not all the tests are done yet - all the unit tests are included but not all of the positive/negative souffle tests are done.

A few notes on improvements:

1. It's not automake ;). No need for bootstrap/configure
2. In general, I think the make structure is cleaner. Right now, the source layout is still automake compatible since I want the two to live side-by-side but there is some room for improvement
3. Clear targets which can be built. See cmake --build <build_dir> --target help to see what's available
4. Testing is improved; all tests are named (so they can be run by name using ctest -R/--tests-regex or by label, e.g. cmake -L/--label-regex. It's now possible to e.g. run just the "interpreted" tests so that testing turnaround is improved. --rerun-failed is your friend, too.
5. I broke out each test into four phases - setup, test, compare stderr/out, compare out files. That way it's easier to spot which part of the test failed. That's why you will now see about 4x more tests.
6. The build is now out-of-source by default and it's possible/easier to have e.g. a release and a debug build side-by-side. Just configure into two separate build dirs.
7. Support from editors (including Intellisense) such as VS Code, CLion and Visual Studio.

There are also performance advantages. On my machine, there are the build/test times:

automake, with -j4: clean build: 3:12.24 total

cmake, with -j4: clean build: 1:55.35 total (This actually does more since it also builds the unit tests)

There's still some work to be done; there is a list of TODO's in the root CMakeFile.txt.

I would appreciate it if someone could give this a spin on Ubuntu/MacOS to see if there are any issues.

TODO before review:

Python code features:

• [x] Finish exposing all current existing interfaces
  • [ ] Symbol table. Interface TBD.
  • [ ] Record table. Interface TBD.
• [x] Handle aux/primary arity, provenance and whether or not it needs to be handled/exposed
• [ ] Handle records
• [ ] Synthesize named tuples for UDTs
• [ ] Support for writing functors in Python (see #1831)
• [ ] Support wrapping of Python objects in Souffle programs

Infra work Items:

• [ ] Make python support conditional
• [ ] Update infra containers to add poetry/nox
• [ ] Linting
• [ ] Mypy
• [ ] More complete nox runner
• [ ] Finish test coverage
• [ ] Documentation
• [ ] Doctests
• [ ] Update README to install poetry and nox
• [ ] Improve distcheck for Python code

This is a work-in-progress to support the build of Souffle on native Windows with Visual Studio.

Current achievement:

• build on Github Actions with windows-latest.
• tests are disabled, they all fail in ctest currently, I did not investigate.

Fixes Main fixes include:

• must use signed integer loop variable in OMP parallel for.
• must explicit many integer conversions.
• must not use dynamically sized array, use unique pointers instead.
• must replace gnu builtins with equivalent msvc builtins.

Other changes:

• getopt / getopt_long no standard on Windows, wrote a replacement function to avoid introducing third-party licensed code.
• some compilation options.

Hi guys,

Consider the following program:

.decl graph(from:number, to:number)
.decl eql(a: number, b: number)
.decl rel(a: number, b: number) btree_delete
.decl C(x:number) btree_delete
.decl D(x:number, y:number)
.decl E(x:number, y:number) btree_delete
.decl a__(a:number, b:number) 

.output a__ // Output node

graph(1, 2).
graph(1, 3).
graph(3, 4).
graph(2, 5).
graph(4, 6).
graph(5, 6).
graph(6, 7).

eql(x,x) :- eql(x,_); eql(_,x).
eql(x,y) :- eql(y,x).
eql(x,z) :- eql(x,y), eql(y,z).
rel(1, 2).
rel(1, 3).
eql(x, x) :- rel(x, _).
eql(2, 3).
rel(a, b) <= rel(c, d) :- eql(a, c), eql(b, d), a <= c, b <= d.

C(1).
D(1, 1).
C(x1) <= C(x2) :- D(x1, x2), x1 <= x2.

E(1,1).
E(1,2).
E(_, x1) <= E(_, x2) :- x1 <= x2.

a__(b, c) :- graph(g, b), !rel(b, d), C(c), E(d, a).

When I run the above program in compiler mode, I get the following result for the relation a__:

$ souffle_59260/src/souffle -w -c orig_rules.dl && cat a__.csv
2	1
3	1
4	1
5	1
6	1
7	1

However, if I add a subgoalE(d, e) in rule a__ to get the a__(b, c) :- graph(g, b), !rel(b, d), C(c), E(d, a), E(d, e)., the result of a__ should not change. But running the following program computes an empty result for a__.

.decl graph(from:number, to:number)
.decl eql(a: number, b: number)
.decl rel(a: number, b: number) btree_delete
.decl C(x:number) btree_delete
.decl D(x:number, y:number)
.decl E(x:number, y:number) btree_delete
.decl a__(a:number, b:number) 

.output a__ // Output node

graph(1, 2).
graph(1, 3).
graph(3, 4).
graph(2, 5).
graph(4, 6).
graph(5, 6).
graph(6, 7).

eql(x,x) :- eql(x,_); eql(_,x).
eql(x,y) :- eql(y,x).
eql(x,z) :- eql(x,y), eql(y,z).
rel(1, 2).
rel(1, 3).
eql(x, x) :- rel(x, _).
eql(2, 3).
rel(a, b) <= rel(c, d) :- eql(a, c), eql(b, d), a <= c, b <= d.

C(1).
D(1, 1).
C(x1) <= C(x2) :- D(x1, x2), x1 <= x2.

E(1,1).
E(1,2).
E(_, x1) <= E(_, x2) :- x1 <= x2.

a__(b, c) :- graph(g, b), !rel(b, d), C(c), E(d, a), E(d, e).

$ souffle_59260/src/souffle -w -c orig_rules.dl && cat a__.csv

FYI, Running both programs in interpreter mode returns:

2	1
3	1
4	1
5	1
6	1
7	1

I am using the latest commit: 592605c21c6b0af9a971499ad9c6a147302184b1

This pull request is aimed to solve issue #573 to enhance Souffle with the implementation of a program interface with SWIG through integrating the work done for the issue as well as adding tests for it. Its aim is to allow other languages to interface Souffle using SWIG. Current supported languages for the SWIG interface is Java and Python. Documentation can be found on https://github.com/chadgavin/souffle/wiki/SWIG.

This pull request is also aimed to solve issue #1075 to fix the tuple insertion bug. A tuple can now only be inserted to a relation which has the same arity and variable type. In addition, SouffleInterface.h is commented and documented by using Doxygen. Documentation can be found on https://github.com/chadgavin/souffle/wiki/C---Interface.

When requesting the provenance of a tuple, Souffle encounters a segmentation fault. The test case is attached. I have encountered this behavior both with the latest release and the repository head.

andersen.zip

To reproduce, run souffle -t explain -F . -D - rules.dl, and request the provenance of pt("v7", "v1").

I am trying to install souffle on OSX 11.6.

I am following the build directions listed here.
However, I am getting the following error when run cmake --build build -j8:

In file included from ~/repos/souffle/src/parser/ParserDriver.cpp:32:
./parser/parser.yy:68:14: fatal error: 'ast/BranchDeclaration.h' file not found
    #include "ast/BranchDeclaration.h"

I also attempted install using homebrew as described here. When running brew install --HEAD souffle-lang/souffle/souffle, I receive the error

==> cmake --build build --target install
Last 15 lines from ~/Library/Logs/Homebrew/souffle/03.cmake:
/tmp/souffle-20211015-55340-1cu7kzf/src/include/souffle/utility/json11.h:290:14: error: expected unqualified-id
    if (std::isfinite(value)) {
             ^
/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX11.3.sdk/usr/include/math.h:155:5: note: expanded from macro 'isfinite'
    ( sizeof(x) == sizeof(float)  ? __inline_isfinitef((float)(x))       \
    ^
15 errors generated.
make[2]: *** [src/CMakeFiles/libsouffle.dir/ast/analysis/ProfileUse.cpp.o] Error 1
make[1]: *** [src/CMakeFiles/libsouffle.dir/all] Error 2
make[1]: *** Waiting for unfinished jobs....
[ 45%] Linking CXX executable test_brie
[ 45%] Linking CXX executable souffleprof
[ 45%] Built target test_brie
[ 45%] Built target souffleprof
make: *** [all] Error 2

Even after following the instructions to update the command line tools.

After the latest additions, I get errors and warnings of the form: Variable ?lastFld only occurs once in file analysis.dl at line 2966 on a file of only 2000 lines. I'm not sure if this is due to wave (suspect not, since I don't use preprocessor directives in that file, but it could be, since I've run into other wave issues without using preprocessor directives) or if it's an issue with the support of multiple heads of rules.

At the moment we rely on cpp to convert Datalog input programs with macros to programs without macros. The conversion is done in main.cpp. The popen() function invokes the cpp and returns a FILE handle on the converted program.

Unfortunately, various systems use different cpp versions/implementations. As a consequence, the behaviour of the macro expansion is not consistent.

My suggestion is to replace cpp with boost's wave library. This library implements a C-Preprocessor and can be added to the Souffle source code. Souffle has a UPL license. Hence I feel that using BOOST with a BSD style license should work (i.e. in general, I believe we cannot add code that has a GPL style license).

Hi,

Consider the following program:

.decl a(A:number)
a(1).
a(2).
a(A1)<=a(A2):-A1<A2.
a(A1)<=a(A2):-A1>A2.
.output a

Souffle has empty result on this program.

The following program is equivalent to this program:

.decl a(A:number)
a(1).
a(A+1):-a(A), A<2.
a(A1)<=a(A2):-A1<A2.
a(A1)<=a(A2):-A1>A2.
.output a

Souffle has the following result:

---------------
a
A
===============
1
===============

Whether they should have equal results, Or maybe I'm wrong to write subsumption like this.

I have another small question, when dealing with subsumption, should it be treated as a separate rule?

The current version of Souffle I use is 3cd802d.

The complexity analysis was ignoring intrinsics operations that can contain functor calls. It had an impact on the reordering of conditions that would move a functor call too early when it is within an intrinsic operation.

fix #2373

Hi,

Consider the following program:

.type typeHejh = symbol
.type typeMrgs = unsigned
.type typeAiik = symbol

.decl tdfw(A:float, B:float, C:float)
.decl hhxs(A:typeHejh, B:typeAiik, C:number, D:typeAiik)
.decl vxeo(A:typeHejh, B:symbol, C:number, D:typeAiik, E:typeAiik, F:typeHejh)

hhxs("40uD340uD3", "40uD3", 4, "40uD3").
tdfw(10.712999999999999, 16.931999999999999, 10.712999999999999).

vxeo(E, C, F, D, C, D) :- tdfw(B, max(A,7.179), --A), hhxs(D, C, F, E).

.output vxeo

This program would hang. I guess it was caused by the unground variable A, but the grammar checker did not find this. If I write this rule b(A):-tdfw(B, max(A,7.179), --A), the grammar can find this error.

The souffle version is 3cd802d, I tried with some older version, also have this issue.

Conditions were sorted nondeterministically in during both the MakeIndex and ReorderConditions RAM transforms. This updates both to use std::stable_sort and eliminates use of pointer comparison to sort Conditions.

When building incremental builds of ddisasm with --generate-many, these changes significantly reduce the number of object files to recompile when a trivial change is made (with the change I am making in my particular configuration, it drops from rebuilding 18 compilation units down to two).

This change fixes source locations with --no-preprocessor and introduces a light virtual file system layer to the parser.

By default the parser sees the real file system (through RealFileSystem). But it is also possible to present any other object that implements the new FileSystem interface. For intance the OverlayFileSystem combines multiple stacked virtual file-system objects (à-la Docker).

Adds a test that demonstrate the use of vfs with the libsouffle.

Some BinaryConstraint atoms can be determined to be impossible during synthesis. This PR introduces a transform to eliminate clauses containing such impossible atoms.

These kinds of atoms are not likely to be written directly, but can easily arise with inlined code.

In ddisasm (with a small work-in-progress change to take greater advantage of this), across its various arch configurations, Souffle generates between 5.0% and 12% fewer lines of C++ with this patch. This yields build time improvements of 2.5% - 10% depending on arch configuration and compiler.

This is my first attempt at adding a transformer pass, so please apply additional scrutiny.