JetBrains/lincheck

unable to inspect throwable type in ExceptionResult

btwilk opened this issue · 9 comments

btwilk commented

lincheck version: 2.20

I have a custom verifier that does:

MyException::class.java.isAssignableFrom(exceptionResult.tClazz)

In lincheck 2.20 this no longer works since tClazz is no longer a member of ExceptionResult

I considered replacing with:

result.throwable is MyException

But this doesn't work since result.throwable has a different classloader than MyException so always returns false.

I can workaround by comparing class names. It would be tricky to workaround in case of an exception hierarchy but my use case doesn't require it for now.

I realize the long term goal is to eliminate the custom classloader altogether, but I figured I'd anyway raise this issue.

@btwilk, thanks for raising the issue! If possible, could you please explain why you need a custom verifier?

btwilk commented

For some reason, it is valid for my system to throw MyException in some cases but these cases aren't determined by operation inputs, so I can't encode when the exceptions should arise into the sequential spec.

Instead, I check this weaker form of linearizability: the operations that don't throw MyException are linearizable.

@btwilk, should the operation that may throw MyException return a result? Can you wrap the operation in a try-catch block, as illustrated below?

@Operation
fun myOperation() = try {
  dataStructure.myOperation()
} catch (e: MyException) {
   Do something
}

btwilk commented

I suppose I could retry the operation on the data structure until it doesn't throw MyException and then just check for standard linearizability. Seems a bit unnatural though. I'd rather directly specify the data structure behavior rather than specifying the behavior of data structure + infinite retries.

btwilk commented

You may mean that I can work around the issue by returning a special value representing that the exception occurred and then check for that value instead of the exception in the custom verifier. That would work (and handles exception hierarchies) but it's awkward.

I suppose I could retry the operation on the data structure until it doesn't throw MyException and then just check for standard linearizability. Seems a bit unnatural though.

You can make it natural by renaming the operation to call<OperationName>UntilSucceeds, making the contract intuitive. Isn't it simpler than writing a custom verifier?

btwilk commented

Some additional context: I have two variants of the test (via inheritance). One never throws and simply checks for standard linearizability. I can avoid introducing unnecessary complexity to this one by customizing the verifier of the other.

Do you find writing a custom verifier simpler than copy-and-pasting the test code?

@btwilk, I encourage you to compare the version with a custom verifier and a version with two similar tests. In the Lincheck team, we strongly believe that users almost never need custom verifiers and consider removing the possibility of specifying ones. Your use case is important, but let's consider the options and check whether you need to write a custom verifier.