Adding Probabilistic Choose() in P

[ankushdesai]

@aman-goel would it help in to have a probabilistic choose()?

Instead of equal probability for the elements in the choose(), having weights assigned to them.
Would it help in coverage? Bug finding?

Thoughts?

[aman-goel]

@ankushdesai Yes, definitely.

I see this as a P language feature. With every data choice made through choose(...), if we allow providing a probability distribution corresponding to each choice, we can easily sample/pick a choice based on this user-provided probability distribution in Coyote/PSym backend. Right now, one has to "mimic" such a distribution manually, e.g.,

// choose true with probability 0.8 and false with probability 0.2

if (choose(100) < 80) {
  return true;
} else {
  return false;
}

With a distribution provided, I think this would be a good feature for users to directly control what region of the state-space is explored by P backends (both Coyote/PSym).

For example, consider TwoPhaseCommit example where a participant returns in the Prepare phase based on

chooseWithWeights(
    (choice = SUCCESS, weight = 0.8),
    (choice = ERROR, weight = 0.2)
)

P backends can then explore the state-space corresponding to SUCCESS with a higher probability compared to ERROR.

E.g., probability of schedules when all participants replied with `SUCCESS` in Prepare phase is
  With 1 client, 1 transaction per client:
    2 participants, 0.8 weight for SUCCESS -> (0.8)^2 = 0.64
    8 participants, 0.8 weight for SUCCESS -> (0.8)^8 = 0.1677
  
    2 participants, equal weights -> (0.5)^2 = 0.25
    8 participants, equal weights -> (0.5)^8 = 0.0039  // much more hard to trigger in a random explorer

For bug finding through Coyote/PSym, this will be an elegant syntax sugar, instead of the "mimic"-style hack.
For coverage of PSym, this would result in a much more accurate measure.
In addition, I expect this to aide in some probabilistic analysis in the future.

[shazqadeer]

I agree that this would be a useful feature to add to P. In addition to all the reasons mentioned by @aman-goel, I mention two other possibilities:

• If the programmer uses probability distribution (some distribution ranging over [0,1]) to control choice, then they can also specify a probability budget for generated executions, e.g., prune executions whose probability dips below a certain small fraction. The probability of an execution will be calculated by simply multiplying the probabilities of all choices encountered along it.
• It could help with better modeling of fair choice which used to exist in P and perhaps still does. Fair choice is useful for modeling liveness specifications which are only satisfied under some fairness constraints. Instead of fair choice, the programmer could use a probabilistic choice. Coupled with the first point, it will provide an easy way around generating very long executions and error traces that are difficult to understand. The MSR team wrote a paper about this problem : https://ieeexplore.ieee.org/document/8102245. Using probabilities is an alternative approach.

[ankushdesai]

@shazqadeer
I have been thinking about adding this to P for a while now. My main concern has always been developers misusing this feature and giving really low probability to error, just like what @aman-goel did (as I had expected ;)). For example, a user comes by and says probability of failure happening in system is 0.001. Let me do that. But if the bug happens in the presence of multiple failures, the probability of finding that bug has now dropped drastically for P.

So the guidance to using probabilistic choose is not to mimic real world behavior, but its actually the other way round. Use the probabilistic choose to give lower weightage to common behavior and bring to surface the less common executions that happen in production.

So my struggle has been, I would like to introduce this feature not as a way to mimic real-world settings but to improve the coverage of less common scenarios.

[shazqadeer]

I don't see how modeling real behavior is a misuse of the feature. At some point in my modeling of a system with P, I may wish to only look at "real" executions and have the P executor do exactly that by giving low probability to "unreal" executions. At another point, I am curious about "unreal" executions so I increase their probability.

Perhaps you are alluding to the problem that we don't know what conclusion to reach when the output of P is not an error trace. Perhaps this problem is solvable by just telling the engineer: don't reach any conclusions when P does not report an error trace.

[ankushdesai]

Yeah, the problem is both telling the engineers when to do what and what is actually happening during exploration. And also, what to conclude at the end of the exploration. Even if no concrete conclusion, they would like to get some feeling that, hey, I gave higher probability to failures so the explorer did explorer "unreal" behaviors in the system.

This is a super fascinating topic and "what did the explorer really do, explore with higher probability" is the million dollar question :)