[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Web engine using TLA+
Hello TLA+ user group!
I'd like to share my latest little use case for our favorite formal verification method: a web engine I am building where some of the core algo's are verified with TLA+:
formal web
As you may know, the Web is already "specified", although only in a semi-formal kind of way; I write "semi-formal" because web standards do use a kind of language that isn't just English, because many things are defined and there is a kind of internal logic to how the standard works, which I think makes is sort of formal even though not based formalized in math.
I have been working with Web standards for about ten years, mainly as a contributor and later maintainer of
Servo, and I have used TLA+ in that context(
example), although just as a kind of "thinking tool" without any tracing in the code.
Also for further context: the Web not only comes with standards, but also with an extensive
test suite for them. But one of the biggest problems we face for example in Servo, is intermittent test results. So yes, the suite covers all standards, but it doesn't cover the actual concurrent logic the way TLA+ can.
So this new project is kind of my answer to the question: "if I could re-architect a web engine today, what would it look like?", and that obviously involves a lot more TLA+, although still only in a few areas were it makes the most sense: parts of web standards and non-standard behavior involving concurrency that goes beyond just posting a message to a queue (there is a lot of task queuing on the web, most of which is too simple to be worth the TLA+ model).
A few words on modelling the rendering loop: in a modern browser engine,
showing some pixels on the screen involves multiple processes--a
process running the web page and usually producing a "display list"
based on the state of the DOM; another process translating various
display lists (in the case of cross origin iframes you have multiple
processes running the different parts of the "page") and other sources
(like video or image frames) into gpu commands; yet another process
presenting the result of running gpu commands--and so such a
multi-process workflow is well positioned to benefit from TLA+
modelling. The challenge in that workflow is that for performance you
want to update the screen as little as possible, but you also do not
want to miss any updates, so there is
a liveness angle to it.
Your feedback would be appreciated, especially pointing out anything wrong.
Gregory
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/38c88301-ecf1-46a6-a0ee-d1d7429890ebn%40googlegroups.com.