search

CMU-18739L-S15 / qira

QEMU Interactive Runtime Analyser
0 stars 0 forks source link

Concolic Executor UI Discussion #5

Open cganas opened 9 years ago

cganas commented 9 years ago

The user interface it self is a much larger issue concerning our integration into Qira.

To have a usable interface we are going to have to have some robust evaluation of the constraints to ensure they are valid. If they aren't, we are going to have to provide meaningful feedback back to the user. See #4.

Another thing we need to focus on is how we are going to update the user. We aren't going to see any performance issues with the toy binaries; however, real programs are going to take much longer. We need to decide how we are going to implement this in an asynchronous manner.

Ideally we would be able to provide users with real-time updates into the progress of our search. The implementation for pub/sub in the web interface has these capabilities. We would just need to periodically publish data in qira_webserver.

cganas commented 9 years ago

Some metrics we could report back to the user are: executors, depth of execution, formula size, and query time provided we do exponential back-off as we discussed in #3.

Are there any other informative metrics we could include? I would assume as long as the interface appears to be doing something meaningful the end user will be happy to hang out while z3 figures out our queries.