search

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
903 stars 198 forks source link

concurrency-related sporadic crashes on ARM architecture #2476

Open quentin opened 5 months ago

quentin commented 5 months ago

I have observed sporadic crashes when multi-threading is enabled on Apple M processors. The weaker memory model of ARM architecture compared to X86 reveals subtle concurrency bugs.

I am suspecting the ConcurrentFlyweight lock-free datastructre ConcurrentFlyweight.h.

One immediate way to mitigate this would be to use stronger std::memory_order::seq_cst here and there at least on ARM architectures.

It would be nice to have an Apple ARM runner for the CI.

quentin commented 5 months ago

There are also some exceptions not handled correctly when building with XCode 15. Some sources on internet suggest to add linker flag -Wl,-ld_classic, I am preparing a CI run for macos14 on Apple M architecture.

christopher-tilt-str commented 5 months ago

Some test failures while running on Mac OS M3 machine: cmake --build build --target test -j 8 (not sure if the number of cores argument makes any difference). built with defaults (OpenMP YES), installed libomp with brew install libomp

Sorry about the huge list here...

The following tests FAILED:
    188 - evaluation/bad_regex_run_souffle (Failed)
    189 - evaluation/bad_regex_compare_std_outputs (Not Run)
    190 - evaluation/bad_regex_compare_csv (Not Run)
    192 - evaluation/bad_regex_c_run_souffle (Failed)
    193 - evaluation/bad_regex_c_compare_std_outputs (Not Run)
    194 - evaluation/bad_regex_c_compare_csv (Not Run)
    526 - evaluation/indexed_inequalities_compare_csv (Failed)
    840 - evaluation/match4_run_souffle (Failed)
    841 - evaluation/match4_compare_std_outputs (Not Run)
    842 - evaluation/match4_compare_csv (Not Run)
    848 - evaluation/match5_run_souffle (Failed)
    849 - evaluation/match5_compare_std_outputs (Not Run)
    850 - evaluation/match5_compare_csv (Not Run)
    852 - evaluation/match5_c_run_souffle (Failed)
    853 - evaluation/match5_c_compare_std_outputs (Not Run)
    854 - evaluation/match5_c_compare_csv (Not Run)
    1211 - evaluation/issue2160_setup (Failed)
    1212 - evaluation/issue2160_run_souffle (Not Run)
    1213 - evaluation/issue2160_compare_std_outputs (Not Run)
    1214 - evaluation/issue2160_compare_csv (Not Run)
    1215 - evaluation/issue2160_c_setup (Failed)
    1216 - evaluation/issue2160_c_run_souffle (Not Run)
    1217 - evaluation/issue2160_c_compare_std_outputs (Not Run)
    1218 - evaluation/issue2160_c_compare_csv (Not Run)
    1411 - semantic/comp_params_inheritance_compare_std_outputs (Failed)
    1414 - semantic/comp_params_inheritance_c_compare_std_outputs (Failed)
    1759 - semantic/load2_compare_std_outputs (Failed)
    1765 - semantic/load3_compare_std_outputs (Failed)
    1771 - semantic/load4_compare_std_outputs (Failed)
    1809 - semantic/load10_compare_std_outputs (Failed)
    1887 - semantic/load_record_invalid_parenthesis_compare_std_outputs (Failed)
    1954 - semantic/negative_numbers_compare_csv (Failed)
    2365 - semantic/subsumption_compare_std_outputs (Failed)
    2368 - semantic/subsumption_c_compare_std_outputs (Failed)
    2827 - semantic/issue1896_setup (Failed)
    2828 - semantic/issue1896_run_souffle (Not Run)
    2829 - semantic/issue1896_compare_std_outputs (Not Run)
    2830 - semantic/issue1896_compare_csv (Not Run)
    2831 - semantic/issue1896_c_setup (Failed)
    2832 - semantic/issue1896_c_run_souffle (Not Run)
    2833 - semantic/issue1896_c_compare_std_outputs (Not Run)
    2834 - semantic/issue1896_c_compare_csv (Not Run)
    2835 - semantic/comp_params_setup (Failed)
    2836 - semantic/comp_params_run_souffle (Not Run)
    2837 - semantic/comp_params_compare_std_outputs (Not Run)
    2838 - semantic/comp_params_compare_csv (Not Run)
    2839 - semantic/comp_params_c_setup (Failed)
    2840 - semantic/comp_params_c_run_souffle (Not Run)
    2841 - semantic/comp_params_c_compare_std_outputs (Not Run)
    2842 - semantic/comp_params_c_compare_csv (Not Run)
    2843 - semantic/issue2416_setup (Failed)
    2844 - semantic/issue2416_run_souffle (Not Run)
    2845 - semantic/issue2416_compare_std_outputs (Not Run)
    2846 - semantic/issue2416_compare_csv (Not Run)
    2847 - semantic/issue2416_c_setup (Failed)
    2848 - semantic/issue2416_c_run_souffle (Not Run)
    2849 - semantic/issue2416_c_compare_std_outputs (Not Run)
    2850 - semantic/issue2416_c_compare_csv (Not Run)
    2851 - semantic/agg_range_setup (Failed)
    2852 - semantic/agg_range_run_souffle (Not Run)
    2853 - semantic/agg_range_compare_std_outputs (Not Run)
    2854 - semantic/agg_range_compare_csv (Not Run)
    2855 - semantic/agg_range_c_setup (Failed)
    2856 - semantic/agg_range_c_run_souffle (Not Run)
    2857 - semantic/agg_range_c_compare_std_outputs (Not Run)
    2858 - semantic/agg_range_c_compare_csv (Not Run)
    2953 - syntactic/input_directive_quotes2_compare_std_outputs (Failed)
    2967 - syntactic/input_directive_quotes_compare_std_outputs (Failed)
    3077 - syntactic/qualifiers4_compare_std_outputs (Failed)
    3080 - syntactic/qualifiers4_c_compare_std_outputs (Failed)
    3105 - syntactic/syntax1_compare_std_outputs (Failed)
    3108 - syntactic/syntax1_c_compare_std_outputs (Failed)
    3129 - syntactic/syntax5_compare_std_outputs (Failed)
    3132 - syntactic/syntax5_c_compare_std_outputs (Failed)
    3135 - syntactic/syntax6_compare_std_outputs (Failed)
    3138 - syntactic/syntax6_c_compare_std_outputs (Failed)
    3147 - syntactic/syntax8_compare_std_outputs (Failed)
    3150 - syntactic/syntax8_c_compare_std_outputs (Failed)
    3159 - syntactic/syntax10_compare_std_outputs (Failed)
    3162 - syntactic/syntax10_c_compare_std_outputs (Failed)
    3265 - syntactic/sourceloc1_compare_std_outputs (Failed)
    3268 - syntactic/sourceloc1_c_compare_std_outputs (Failed)
    3271 - syntactic/sourceloc2_compare_std_outputs (Failed)
    3274 - syntactic/sourceloc2_c_compare_std_outputs (Failed)
    3283 - syntactic/sourceloc4_compare_std_outputs (Failed)
    3286 - syntactic/sourceloc4_c_compare_std_outputs (Failed)
    3289 - syntactic/sourceloc5_compare_std_outputs (Failed)
    3292 - syntactic/sourceloc5_c_compare_std_outputs (Failed)
    3295 - syntactic/unterminated_comment_compare_std_outputs (Failed)
    3298 - syntactic/unterminated_comment_c_compare_std_outputs (Failed)
    3299 - syntactic/annotations_setup (Failed)
    3300 - syntactic/annotations_run_souffle (Not Run)
    3301 - syntactic/annotations_compare_std_outputs (Not Run)
    3302 - syntactic/annotations_compare_csv (Not Run)
    3303 - syntactic/annotations_c_setup (Failed)
    3304 - syntactic/annotations_c_run_souffle (Not Run)
    3305 - syntactic/annotations_c_compare_std_outputs (Not Run)
    3306 - syntactic/annotations_c_compare_csv (Not Run)
    3307 - syntactic/doc_comment_setup (Failed)
    3308 - syntactic/doc_comment_run_souffle (Not Run)
    3309 - syntactic/doc_comment_compare_std_outputs (Not Run)
    3310 - syntactic/doc_comment_compare_csv (Not Run)
    3311 - syntactic/doc_comment_c_setup (Failed)
    3312 - syntactic/doc_comment_c_run_souffle (Not Run)
    3313 - syntactic/doc_comment_c_compare_std_outputs (Not Run)
    3314 - syntactic/doc_comment_c_compare_csv (Not Run)
    3315 - syntactic/doc_comment_dangling1_setup (Failed)
    3316 - syntactic/doc_comment_dangling1_run_souffle (Not Run)
    3317 - syntactic/doc_comment_dangling1_compare_std_outputs (Not Run)
    3318 - syntactic/doc_comment_dangling1_compare_csv (Not Run)
    3319 - syntactic/doc_comment_dangling1_c_setup (Failed)
    3320 - syntactic/doc_comment_dangling1_c_run_souffle (Not Run)
    3321 - syntactic/doc_comment_dangling1_c_compare_std_outputs (Not Run)
    3322 - syntactic/doc_comment_dangling1_c_compare_csv (Not Run)
    3323 - syntactic/doc_comment_dangling2_setup (Failed)
    3324 - syntactic/doc_comment_dangling2_run_souffle (Not Run)
    3325 - syntactic/doc_comment_dangling2_compare_std_outputs (Not Run)
    3326 - syntactic/doc_comment_dangling2_compare_csv (Not Run)
    3327 - syntactic/doc_comment_dangling2_c_setup (Failed)
    3328 - syntactic/doc_comment_dangling2_c_run_souffle (Not Run)
    3329 - syntactic/doc_comment_dangling2_c_compare_std_outputs (Not Run)
    3330 - syntactic/doc_comment_dangling2_c_compare_csv (Not Run)
    3331 - syntactic/doc_comment_dangling3_setup (Failed)
    3332 - syntactic/doc_comment_dangling3_run_souffle (Not Run)
    3333 - syntactic/doc_comment_dangling3_compare_std_outputs (Not Run)
    3334 - syntactic/doc_comment_dangling3_c_setup (Failed)
    3335 - syntactic/doc_comment_dangling3_c_run_souffle (Not Run)
    3336 - syntactic/doc_comment_dangling3_c_compare_std_outputs (Not Run)
    3385 - interface/lattice1_setup (Failed)
    3386 - interface/lattice1_run_souffle (Not Run)
    3387 - interface/lattice1_compare_std_outputs (Not Run)
    3388 - interface/lattice1_compare_csv (Not Run)
    3389 - interface/lattice1_c_setup (Failed)
    3390 - interface/lattice1_c_run_souffle (Not Run)
    3391 - interface/lattice1_c_compare_std_outputs (Not Run)
    3392 - interface/lattice1_c_compare_csv (Not Run)
    3393 - interface/lattice1_C_setup (Failed)
    3394 - interface/lattice1_C_run_souffle (Not Run)
    3395 - interface/lattice1_C_compare_std_outputs (Not Run)
    3396 - interface/lattice1_C_compare_csv (Not Run)
    3397 - interface/lattice2_setup (Failed)
    3398 - interface/lattice2_run_souffle (Not Run)
    3399 - interface/lattice2_compare_std_outputs (Not Run)
    3400 - interface/lattice2_compare_csv (Not Run)
    3401 - interface/lattice2_c_setup (Failed)
    3402 - interface/lattice2_c_run_souffle (Not Run)
    3403 - interface/lattice2_c_compare_std_outputs (Not Run)
    3404 - interface/lattice2_c_compare_csv (Not Run)
    3405 - interface/lattice2_C_setup (Failed)
    3406 - interface/lattice2_C_run_souffle (Not Run)
    3407 - interface/lattice2_C_compare_std_outputs (Not Run)
    3408 - interface/lattice2_C_compare_csv (Not Run)
    3409 - interface/lattice3_setup (Failed)
    3410 - interface/lattice3_run_souffle (Not Run)
    3411 - interface/lattice3_compare_std_outputs (Not Run)
    3412 - interface/lattice3_compare_csv (Not Run)
    3413 - interface/lattice3_c_setup (Failed)
    3414 - interface/lattice3_c_run_souffle (Not Run)
    3415 - interface/lattice3_c_compare_std_outputs (Not Run)
    3416 - interface/lattice3_c_compare_csv (Not Run)
    3417 - interface/lattice3_C_setup (Failed)
    3418 - interface/lattice3_C_run_souffle (Not Run)
    3419 - interface/lattice3_C_compare_std_outputs (Not Run)
    3420 - interface/lattice3_C_compare_csv (Not Run)
quentin commented 5 months ago

I have changed all memory_order to memory_order_seq_cst and I still reproduce a crash.

I build on M1 with llvm17 openmp library. Then run evaluation/cprog4 test in a loop until it crashes with this message: 

OMP: Error #13: Assertion failure at kmp_dispatch.cpp(1298).
OMP: Hint Please submit a bug report with this message, compile and run commands used, and machine configuration info including native compiler and operating system versions. Faster response will be obtained by including all program sources. For information on submitting this issue, please see https://bugs.llvm.org/.
Abort trap: 6 (core dumped)

This assertion failure is known: https://github.com/llvm/llvm-project/issues/54422

So maybe, after all, the crashes that I observe are not due to Souffle code but the llvm openmp library.

Note that the Souffle CI builds with gcc, so it might be safe to enable openmp in the CI.