Streaming messages from ViperCoreServer about viperserver HOT 8 CLOSED

" ... or is it the case that the streaming starts only when the future returned by lookupJob is complete."

Yes, this is the case.

" ... if the current implementation of streamMessages actually streams messages as soon as they are available in the source queue, ..."

Yes, this is the case as well. ;)

I'll admit that this sounds contradictive. But there's a crux: handle_future is completed as soon as possible:

In summary: we indeed only start streaming once the handle_future is completed, but this is not a problem as the future is immediately completed.

from viperserver.

Addendum 1

In case you wonder why there's a future at all if it is immediately resolved: When communicating with actors the answers always come back as Future[Any]. Whatever we do, we have to wait back for that future before doing anything related to a handle.

Addendum 2

This comment is wrong.

Let me know if you agree and I'll correct the comment.

from viperserver.

Thanks, @WissenIstNacht , for clarifying this. I was indeed confused by the comments above the definition of lookupJob. Could you please fix the misleading comment and add some new ones to make it clear which future does what?

Since lookupJob does not tell us whether the verification is in progress, is there some other method in the API that can be used for getting something like Future[Bool], indcating that the job has been completed? We need such a future to be generated by a method that does not consume the messages because otherwise one cannot stream the messages and obtain the completion future for the same job (i.e. getResultsFuture and streamMessages won't work for the same job ID).

from viperserver.

Sure, I'll add the necessary comments.

Since lookupJob does not tell us whether the verification is in progress, is there some other method in the API that can be used for getting something like Future[Bool], indcating that the job has been completed?

No, at the moment the API does not support this.

from viperserver.

Thanks for adding the comments.

I would like to propose the following new signature for the method streamMessages:

def streamMessages(jid: Int, clientActor: ActorRef): Option[Future[Bool]]

The return type should be None in case the job with this jid was never started, and would be Some(completionFuture) otherwise. completionFuture will be resolved to overallResult as soon as the verification is completed for the entire AST. True would mean overall success and False would mean that something there are messages that are not consumed yet or that new messages might still be produced (i.e., verification in progress).

Could you add this functionality, please?

from viperserver.

I would like to voice a few remarks/questions on this proposal:

What exactly should the Boolean type express in you signature? When should the Future be completed?

I think a Boolean should answer a question with yes or no. From your description I get the feeling that it answers two different questions, one with yes and one with no. Also, a state of (in)completion is exactly what an (in)completed Future expresses. Why then put the fact that a Future is (not) resolved into the Boolean type that is contained in that Future?

Also, while the API does not provide this information, it doesn't mean the information does not exist. In fact, the flow of information was precisely set up in such a way that it does. A client who uses an actor to communicate with ViperCoreServer will get a stream of messages where the last message is a overall success/failure. This indicates all you're asking for: The result of the process, the fact that it's over and even whether or not a verification job exists (i.e., has been started) or not.

I feel like what you proposed should be the return type of a method called getOverallVerificationResults and should not be the return type of streamMessages. Recall, the point of streamMessages was to attach an actor to ViperCoreServer and "continue" the stream/actor-based architecture. In my view, adding this signature is not in line with the API's design.

from viperserver.

Hi Valentin,

These are valid concerns, so let me try to address them (the order is random).

Also, while the API does not provide this information, it doesn't mean the information does not exist. In fact, the flow of information was precisely set up in such a way that it does. A client who uses an actor to communicate with ViperCoreServer will get a stream of messages where the last message is a overall success/failure. This indicates all you're asking for: The result of the process, the fact that it's over and even whether or not a verification job exists (i.e., has been started) or not.

I agree that one could use an actor to pattern match on Overall results and find out when the verification is completed. So you are right that, in principle, one could circumvent the issue. However, I think the API should provide a more streightforward way to get the information about when the verification job has ended. This information is needed for any client that uses streams, so let's provide it directly instead of asking the client to retrieve it on their own.

I feel like what you proposed should be the return type of a method called getOverallVerificationResults and should not be the return type of streamMessages. Recall, the point of streamMessages was to attach an actor to ViperCoreServer and "continue" the stream/actor-based architecture. In my view, adding this signature is not in line with the API's design.

Actually, no: when the client is interested only in the overall results (and not the intermediate ones), then they would get the information about the end of this verification job for free. This is what happens in the scenario in which the client uses getResultsFuture — that scenario seems to be completely covered with the code that we have right now. Conversely, the scenario in which we are streaming the messages requires the client to know when the stream is completed. This information is provided by Akka, but we have to wrap it into our own API because we don't want the client to have to understand Akka-specific concepts e.g. SourceQueueWithComplete. The next question is — how do we wrap this information into our own API? Do we create a new method that returns the abovementioned future? We could, but then each time the client wants to stream the messages they would need to call two methods instead of one. so my suggestion would be to not add another method and to instead use the (currently unused) return type of streamMessages. Even if there would be a client that doesn't care about the completion of the verification job, they could just ignore the return value of streamMessages and carry on just like they could right now.

What exactly should the Boolean type express in you signature? When should the Future be completed?

I think a Boolean should answer a question with yes or no. From your description I get the feeling that it answers two different questions, one with yes and one with no. Also, a state of (in)completion is exactly what an (in)completed Future expresses. Why then put the fact that a Future is (not) resolved into the Boolean type that is contained in that Future?

There are four possible designs that come to mind. It seems that you don't disagree with the Option part of the return type, so I'll assume in the following that (a) we have this option as the return type of streamMessages; None means that the job with such jid has never been started; Some(x) means that the job has been started, and there's a future, x, that is attached to this job.

1. We could use the type Future[Unit] to avoid attaching any semantics to the value and only keep the semantics of the future (not resolved = verification in progress; resolved = verification has been completed or verification has been interrupted, e.g., due to a stack trace/ raised exception).

2. We could use the type Future[Bool] where the Boolean flag indicates which of the two case occured (true = normal completion, i.e., no stack trace; false = there has been an exception/ something crashed/ the job could not be booked due to constraints in ViperServer, e.g. we have reached the max number of actively running jobs).

3. Alternitively, we could use the type Future[Bool] where the Boolean flag indicates if the verification did not crash (using the definition above) and all verification targets have been successfully verified. This is my initial idea that I described in my previous comment. However, I now see option 2 as a more meaningful way of using the flag.

4. Finally, we culd return the verrification resuts as-is and let the user pattern match to find out if it was a success or something went wrong. This is not what we want because for the case in which the user wants to get just one future in the end of the verification process, we already provide the utility method getResultsFuture from ViperCoreServerUtils.

from viperserver.

Thanks for implementing this API change.

from viperserver.