1

私はJavaJNIを使​​用して、使用しているフレームワークにZ3SolverC-Apiを統合しています。今、私は次のメッセージでセグメンテーション違反を起こしている-

#
# A fatal error has been detected by the Java Runtime Environment:
#
#  SIGSEGV (0xb) at pc=0x664c4af0, pid=10878, tid=3060636480
#
# JRE version: 7.0_09-b30
# Java VM: OpenJDK Server VM (23.2-b09 mixed mode linux-x86 )
# Problematic frame:
# C  [libSpdfZ3.so+0x634af0]  small_object_allocator::allocate(unsigned int)+0x40
#
# Failed to write core dump. Core dumps have been disabled. To enable core dumping, try "ulimit -c unlimited" before starting Java again
#
# An error report file with more information is saved as:
# /home/rajtendulkar/workspace/Java-WorkSpace/spdf-compiler_with_Yices_and_Z3_StaticLib/hs_err_pid10878.log
#
# If you would like to submit a bug report, please include
# instructions on how to reproduce the bug and visit:
#   https://bugs.launchpad.net/ubuntu/+source/openjdk-7/
# The crash happened outside the Java Virtual Machine in native code.
# See problematic frame for where to report the bug.
#

ログファイル内では、Z3のコンテキストが割り当てられている1つの呼び出しを指します。基本的には、メモリが割り当てられた初期化ルーチンです。

このセグメンテーション違反の原因を理解したいと思います。私のプログラムは一度実行すると正常に動作することを述べておきたいと思います。ただし、このようにforループで実行すると-

for (int i=0;i<5;i++)
{
     // create z3 context
     Z3Object obj = new Z3Object();
     ...
     ... 
     .. do some exploration here ..
     ...  
     ...
     ...     
}

これがメモリの割り当てやメモリの不足などと関係があるのか​​どうかを考えていますか？

これをデバッグする方法についてのポインタはありがたいです。

編集 ：

コードをデバッグしてゆっくりと進めようとすると、この問題は発生しません。同様に、forループの最後に5秒の遅延を設定すると、セグメントが取得されません。障害。それで、それは並行性の問題と関連している可能性がありますか？

4

1 に答える 1

2

Z3用のカスタムJNIバインディングを開発しているようです。Z3には、次のリリースの1つで独自のバインディングが付属することに注意してください。これはすでにCodeplexの「不安定な」ブランチに含まれており、インスピレーションとして、あるいは代替として役立つ可能性があります。

z3.dllから取得したオブジェクトは、正しく参照カウントされる必要があることに注意してください。これは、使用されるガベージコレクターの種類によってはかなり注意が必要です。私の最初の疑いは、プログラムが気付かないうちにオブジェクトが（Z3によって）収集されるか（たとえば、参照カウントが同期しなくなるため）、またはガベージコレクターがZ3がしない順序でオブジェクトを破棄しようとしていることです。 t予測します（たとえば、関連するすべてのオブジェクトが破棄される前にコンテキストを破棄します）。

並行性の問題はおそらく独自のプログラムによるものではありませんが、ガベージコレクターが並行しているためです（私が正しく覚えていれば、Javaの新しいバージョンには実際には4つの異なるバージョンがあり、ホストシステムに応じてそれらから選択します。問題の原因）。

于 2013-02-05T17:15:37.863 に答える