Improving Apple Silicon Build

[tquatmann]

• Use updated Eigen version to avoid a bug in old version 3.3.9. Since the new version is buggy in other cases (issue Issues with gcc and Eigen 3.4.0 #162), the workaround is to conditionally build the new version only for Apple Silicon
• Changed warning from "Not supported" to "experimental support"
• Changelog Entry

[sjunges]

LGTM!

[culechetoo]

Hi

I followed the steps mentioned in #274. But while testing, I am still getting a fail for the following test:

17 - run-test-modelchecker-multiobjective (SEGFAULT)

I noticed that my carl build used version 3.3.4 of Eigen. Could that be an issue? If so, can you please advise a workaround? Let me know if you need any more details.

Thanks

[tquatmann]

Hi

this is exactly the error that (at least for me) was resolved when using the updated Eigen version. The Eigen version used by Carl should not be relevant here.

Could you try the following:

• remove the build folder (to be sure that there are no remains of Eigen v3.3.9)
• build storm again, as before. During cmake .. make sure that there is the line:

-- Storm - Including Eigen 3.4.0 commit b0eded878d5d162d61583a286c0d8a45406ad1bc.

Thanks a lot!

[culechetoo]

Hi

Unfortunately I'm still getting the same error. I have attached the output of the cmake command below.

build % cmake .. -DSTORM_PORTABLE=ON -DSTORM_USE_CLN_RF=OFF -DSTORM_CARL_DIR_HINT=~/Projects/carl/build
-- The CXX compiler identification is AppleClang 14.0.3.14030022
-- The C compiler identification is AppleClang 14.0.3.14030022
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Check for working CXX compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/c++ - skipped
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Check for working C compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/cc - skipped
-- Detecting C compile features
-- Detecting C compile features - done
-- Storm - CMake install dir: /usr/local/lib/CMake/storm
-- Storm - Building RELEASE version.
-- Storm - Could not find ccache.
-- Storm - Detected operating system Mac OS.
-- Storm - Detected that target system uses Apple Silicon.
CMake Warning at CMakeLists.txt:194 (message):
  Compiling natively on Apple Silicon is experimental.  Pleare report issues
  to support@stormchecker.org.  For more information visit
  https://www.stormchecker.org/documentation/obtain-storm/apple-silicon.html


-- Storm - Assuming extension for shared libraries: .dylib
-- Storm - Assuming extension for static libraries: .a
-- Storm - Build static libraries.
CMake Warning at CMakeLists.txt:247 (message):
  Disabling stack checks for AppleClang version 11.0.0 or higher.


-- Storm - Enabling link-time optimizations.
-- Performing Test COMPILER_C_WORKS
-- Performing Test COMPILER_C_WORKS - Success
-- Performing Test COMPILER_CXX_WORKS
-- Performing Test COMPILER_CXX_WORKS - Success
-- Storm - Using compiler configuration AppleClang 14.0.3.14030022.
-- Storm - Building external resources with 5 job(s) in parallel.
-- Storm - Including Eigen 3.4.0 commit b0eded878d5d162d61583a286c0d8a45406ad1bc.
-- Storm - Using workaround for Boost 1.81
-- Storm - Using boost 108100 (library version 1_81).
-- Storm - Including ExprTk.
-- Storm - Including Parallel Hashmap.
-- Storm - Including cpphoafparser 0.99.2
-- Storm - Including ModernJSON.
-- Storm - Linking with Z3 (version 4.12.1). (Z3 version supports optimization)
-- Storm - Using system version of glpk.
-- Storm - Linking with glpk 5.0
CMake Warning at resources/3rdparty/include_cudd.cmake:41 (message):
  There are some known issues compiling CUDD on some setups.  We implemented
  a workaround that mostly works, but if you still have problems compiling
  CUDD, especially if you do not use the default compiler of your system,
  please contact the Storm developers.
Call Stack (most recent call first):
  resources/3rdparty/CMakeLists.txt:287 (include)
  CMakeLists.txt:473 (include)


-- Storm - Linking with CUDD 3.0.0.
-- Storm - Found carl-storm version
-- Storm - Use system version of carl.
-- Storm - Linking with preinstalled carl 14.22 (include: /Users/chetoo/Projects/carl/src, library lib_carl, CARL_USE_CLN_NUMBERS: OFF, CARL_USE_GINAC: OFF).
CMake Warning at resources/3rdparty/CMakeLists.txt:408 (message):
  Uses an outdated repo for Carl.  Carl is now hosted at
  https://github.com/moves-rwth/carl-storm
Call Stack (most recent call first):
  CMakeLists.txt:473 (include)


-- Storm - Use system version of xerces.
-- Storm (GSPN) - Linking with Xerces-c 3.2.4: /opt/homebrew/lib/libxerces-c.dylib
CMake Warning at resources/3rdparty/include_spot.cmake:23 (message):
  Storm - Could not find Spot.  Model checking of LTL formulas (beyond PCTL)
  will not be supported.  You may want to set cmake option
  STORM_USE_SPOT_SHIPPED to install Spot automatically.  If you already
  installed Spot, consider setting cmake option SPOT_ROOT.  Unset
  STORM_USE_SPOT_SYSTEM to silence this warning.
Call Stack (most recent call first):
  resources/3rdparty/CMakeLists.txt:580 (include)
  CMakeLists.txt:473 (include)


-- Storm - Using shipped version of sylvan.
-- Storm - Linking with sylvan.
-- Could NOT find Doxygen (missing: DOXYGEN_EXECUTABLE) 
-- Storm - Version is 1.7.1 (dev) (version 1.7.0 + 112 commits), building from git: 66cede1ae9f34aea0382bbe300c3bbddf30cf466 (dirty: DirtyState::Clean).
-- Registered with cmake
-- Configuring done (1.7s)
-- Generating done (0.3s)
-- Build files have been written to: /Users/chetoo/Projects/storm/build

[tquatmann]

Unfortunately, I can not reproduce this. Depending what you're doing with Storm, this issue likely does not affect you, though.
We can still try to narrow this down a bit. If possible, could you send me the full output of the following series of commands which will tell us where exactly things go wrong:

• cd storm/build/bin
• lldb -- ./test-modelchecker-multiobjective This might need your system root password
• Wait a few seconds until lldb starts. Then, type process launch and hit enter
• Wait while the test binary is executed until the error occurs
• Type bt to show the backtrace
• Type q to quit lldb

Thanks a lot!

[culechetoo]

Hi

Here is the output. Do let me know if you need anything else from me.

(base) chetoo@10-16-203-77 bin % lldb -- ./test-modelchecker-multiobjective
(lldb) target create "./test-modelchecker-multiobjective"
Current executable set to '/Users/chetoo/Projects/storm/build/bin/test-modelchecker-multiobjective' (arm64).
(lldb) process launch
Process 95892 launched: '/Users/chetoo/Projects/storm/build/bin/test-modelchecker-multiobjective' (arm64)
[==========] Running 36 tests from 7 test suites.
[----------] Global test environment set-up.
[----------] 3 tests from MultiObjectiveSchedRestModelCheckerTest
[ RUN      ] MultiObjectiveSchedRestModelCheckerTest.steps
[       OK ] MultiObjectiveSchedRestModelCheckerTest.steps (1600 ms)
[ RUN      ] MultiObjectiveSchedRestModelCheckerTest.mecs
[       OK ] MultiObjectiveSchedRestModelCheckerTest.mecs (1208 ms)
[ RUN      ] MultiObjectiveSchedRestModelCheckerTest.compromise
[       OK ] MultiObjectiveSchedRestModelCheckerTest.compromise (8494 ms)
[----------] 3 tests from MultiObjectiveSchedRestModelCheckerTest (11303 ms total)

[----------] 3 tests from SparseDtmcMultiDimensionalRewardUnfoldingTest
[ RUN      ] SparseDtmcMultiDimensionalRewardUnfoldingTest.cost_bounded_die
[       OK ] SparseDtmcMultiDimensionalRewardUnfoldingTest.cost_bounded_die (11 ms)
[ RUN      ] SparseDtmcMultiDimensionalRewardUnfoldingTest.cost_bounded_leader
[       OK ] SparseDtmcMultiDimensionalRewardUnfoldingTest.cost_bounded_leader (17 ms)
[ RUN      ] SparseDtmcMultiDimensionalRewardUnfoldingTest.cost_bounded_crowds
[       OK ] SparseDtmcMultiDimensionalRewardUnfoldingTest.cost_bounded_crowds (18 ms)
[----------] 3 tests from SparseDtmcMultiDimensionalRewardUnfoldingTest (46 ms total)

[----------] 1 test from SparseMaCbMultiObjectiveModelCheckerTest
[ RUN      ] SparseMaCbMultiObjectiveModelCheckerTest.server
[       OK ] SparseMaCbMultiObjectiveModelCheckerTest.server (28 ms)
[----------] 1 test from SparseMaCbMultiObjectiveModelCheckerTest (28 ms total)

[----------] 8 tests from SparseMaPcaaMultiObjectiveModelCheckerTest
[ RUN      ] SparseMaPcaaMultiObjectiveModelCheckerTest.serverRationalNumbers
Process 95892 stopped
* thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x7)
    frame #0: 0x000000010062667c libgmp.10.dylib`__gmpz_init_set + 24
libgmp.10.dylib`:
->  0x10062667c <+24>: ldr    w22, [x1, #0x4]
    0x100626680 <+28>: cmp    w22, #0x0
    0x100626684 <+32>: cneg   w21, w22, mi
    0x100626688 <+36>: cmp    w21, #0x1
Target 0: (test-modelchecker-multiobjective) stopped.
(lldb) bt
* thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x7)
  * frame #0: 0x000000010062667c libgmp.10.dylib`__gmpz_init_set + 24
    frame #1: 0x0000000103cf3f40 libstorm.dylib`Eigen::internal::binary_evaluator<Eigen::CwiseBinaryOp<Eigen::internal::scalar_product_op<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, __gmp_expr<__mpq_struct [1], __mpq_struct [1]> >, Eigen::Transpose<Eigen::Block<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1> const, 1, -1, false> const> const, Eigen::Block<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1> const, -1, 1, true> const>, Eigen::internal::IndexBased, Eigen::internal::IndexBased, __gmp_expr<__mpq_struct [1], __mpq_struct [1]>, __gmp_expr<__mpq_struct [1], __mpq_struct [1]> >::coeff(long, long) const + 64
    frame #2: 0x0000000104cefafc libstorm.dylib`Eigen::internal::dense_assignment_loop<Eigen::internal::restricted_packet_dense_assignment_kernel<Eigen::internal::evaluator<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1> >, Eigen::internal::evaluator<Eigen::Product<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1>, Eigen::Inverse<Eigen::FullPivLU<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1>, int> >, 1> >, Eigen::internal::assign_op<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, __gmp_expr<__mpq_struct [1], __mpq_struct [1]> > >, 0, 0>::run(Eigen::internal::restricted_packet_dense_assignment_kernel<Eigen::internal::evaluator<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1> >, Eigen::internal::evaluator<Eigen::Product<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1>, Eigen::Inverse<Eigen::FullPivLU<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1>, int> >, 1> >, Eigen::internal::assign_op<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, __gmp_expr<__mpq_struct [1], __mpq_struct [1]> > >&) + 176
    frame #3: 0x0000000104cef900 libstorm.dylib`void Eigen::internal::call_restricted_packet_assignment_no_alias<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1>, Eigen::Product<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1>, Eigen::Inverse<Eigen::FullPivLU<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1>, int> >, 1>, Eigen::internal::assign_op<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, __gmp_expr<__mpq_struct [1], __mpq_struct [1]> > >(Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1>&, Eigen::Product<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1>, Eigen::Inverse<Eigen::FullPivLU<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1>, int> >, 1> const&, Eigen::internal::assign_op<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, __gmp_expr<__mpq_struct [1], __mpq_struct [1]> > const&) + 108
    frame #4: 0x0000000104ceb57c libstorm.dylib`void Eigen::internal::generic_product_impl<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1>, Eigen::Inverse<Eigen::FullPivLU<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1>, int> >, Eigen::DenseShape, Eigen::DenseShape, 3>::eval_dynamic<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1>, Eigen::internal::assign_op<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, __gmp_expr<__mpq_struct [1], __mpq_struct [1]> > >(Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1>&, Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1> const&, Eigen::Inverse<Eigen::FullPivLU<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1>, int> > const&, Eigen::internal::assign_op<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, __gmp_expr<__mpq_struct [1], __mpq_struct [1]> > const&) + 156
    frame #5: 0x0000000104ceb498 libstorm.dylib`void Eigen::internal::generic_product_impl<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1>, Eigen::Inverse<Eigen::FullPivLU<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1>, int> >, Eigen::DenseShape, Eigen::DenseShape, 8>::evalTo<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1> >(Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1>&, Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1> const&, Eigen::Inverse<Eigen::FullPivLU<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1>, int> > const&) + 160
    frame #6: 0x0000000104ceac8c libstorm.dylib`Eigen::PlainObjectBase<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1> >::PlainObjectBase<Eigen::Product<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1>, Eigen::Inverse<Eigen::FullPivLU<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1>, int> >, 0> >(Eigen::DenseBase<Eigen::Product<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1>, Eigen::Inverse<Eigen::FullPivLU<Eigen::Matrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, -1, -1, 0, -1, -1>, int> >, 0> > const&) + 128
    frame #7: 0x0000000104ce7058 libstorm.dylib`storm::storage::geometry::NativePolytope<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >::affineTransformation(std::__1::vector<std::__1::vector<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, std::__1::allocator<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> > >, std::__1::allocator<std::__1::vector<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, std::__1::allocator<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> > > > > const&, std::__1::vector<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, std::__1::allocator<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> > > const&) const + 528
    frame #8: 0x00000001042b93a8 libstorm.dylib`std::__1::shared_ptr<storm::storage::geometry::Polytope<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> > > storm::modelchecker::multiobjective::transformObjectivePolytopeToOriginal<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, __gmp_expr<__mpq_struct [1], __mpq_struct [1]> >(std::__1::vector<storm::modelchecker::multiobjective::Objective<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >, std::__1::allocator<storm::modelchecker::multiobjective::Objective<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> > > >, std::__1::shared_ptr<storm::storage::geometry::Polytope<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> > > const&) + 1076
    frame #9: 0x0000000104366fbc libstorm.dylib`storm::modelchecker::multiobjective::SparsePcaaParetoQuery<storm::models::sparse::MarkovAutomaton<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, storm::models::sparse::StandardRewardModel<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> > >, __gmp_expr<__mpq_struct [1], __mpq_struct [1]> >::check(storm::Environment const&) + 1608
    frame #10: 0x000000010434cffc libstorm.dylib`std::__1::unique_ptr<storm::modelchecker::CheckResult, std::__1::default_delete<storm::modelchecker::CheckResult> > storm::modelchecker::multiobjective::performMultiObjectiveModelChecking<storm::models::sparse::MarkovAutomaton<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, storm::models::sparse::StandardRewardModel<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> > > >(storm::Environment const&, storm::models::sparse::MarkovAutomaton<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, storm::models::sparse::StandardRewardModel<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> > > const&, storm::logic::MultiObjectiveFormula const&) + 2116
    frame #11: 0x000000010007d6b0 test-modelchecker-multiobjective`SparseMaPcaaMultiObjectiveModelCheckerTest_serverRationalNumbers_Test::TestBody() + 652
    frame #12: 0x0000000100052524 test-modelchecker-multiobjective`void testing::internal::HandleSehExceptionsInMethodIfSupported<testing::Test, void>(testing::Test*, void (testing::Test::*)(), char const*) + 132
    frame #13: 0x0000000100015b50 test-modelchecker-multiobjective`void testing::internal::HandleExceptionsInMethodIfSupported<testing::Test, void>(testing::Test*, void (testing::Test::*)(), char const*) + 96
    frame #14: 0x0000000100015aa0 test-modelchecker-multiobjective`testing::Test::Run() + 192
    frame #15: 0x0000000100016b30 test-modelchecker-multiobjective`testing::TestInfo::Run() + 244
    frame #16: 0x0000000100017c20 test-modelchecker-multiobjective`testing::TestSuite::Run() + 276
    frame #17: 0x0000000100025978 test-modelchecker-multiobjective`testing::internal::UnitTestImpl::RunAllTests() + 1008
    frame #18: 0x0000000100058948 test-modelchecker-multiobjective`bool testing::internal::HandleSehExceptionsInMethodIfSupported<testing::internal::UnitTestImpl, bool>(testing::internal::UnitTestImpl*, bool (testing::internal::UnitTestImpl::*)(), char const*) + 132
    frame #19: 0x000000010002534c test-modelchecker-multiobjective`bool testing::internal::HandleExceptionsInMethodIfSupported<testing::internal::UnitTestImpl, bool>(testing::internal::UnitTestImpl*, bool (testing::internal::UnitTestImpl::*)(), char const*) + 96
    frame #20: 0x0000000100025238 test-modelchecker-multiobjective`testing::UnitTest::Run() + 216
    frame #21: 0x00000001000a4764 test-modelchecker-multiobjective`main + 148
    frame #22: 0x00000001ab0ffe50 dyld`start + 2544
(lldb) q

[tquatmann]

This (to me) does look like an issue in Eigen but I can't say for sure. I'll try a few more things to reproduce it.

Thanks for your help so far, much appreciated!