JetBrains / lincheck

Framework for testing concurrent data structures
Mozilla Public License 2.0
555 stars 31 forks source link

unable to inspect throwable type in ExceptionResult #203

Closed btwilk closed 6 months ago

btwilk commented 1 year ago

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.

ndkoval commented 1 year ago

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

btwilk commented 1 year ago

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.

ndkoval commented 1 year ago

@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 1 year ago

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 1 year ago

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.

ndkoval commented 1 year ago

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 1 year ago

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.

ndkoval commented 1 year ago

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

ndkoval commented 1 year ago

@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.