3 ms·

To be clear, P is used for validating the asynchronous state machines used by the Windows USB drivers, and not for implementing the drivers, which are written i

To be clear, P is used for validating the asynchronous state machines used by the Windows USB drivers, and not for implementing the drivers, which are written in C. And the USB driver stack implementation is same for both Windows 8 & and Windows 10, so the answer to your question is - yes.

Camillo 10y ago
The README says: "P has been used to implement and validate the USB device driver stack that ships with Microsoft Windows 8 and Windows Phone". It's not clear from your answer. Does Windows ship with a "USB device driver stack" written in P, yes or no?
- nickpsecurity 10y ago
  The way these normally work is that they do the state machine in the domain-specific language, verify it, auto-generate code in something like C, and compile that. That's almost all of them since it's easy to go from models to code automatically for state machines. The Github page says: "Not only can a P program be compiled into executable code, but it can also be validated using systematic testing. P has been used to implement and validate the USB device driver stack that ships with Microsoft Windows 8 and Windows Phone. " That indicates they modeled it in P with their tool compiling the P specs into some executable. The individual functions the state machine calls would be other C or assembly functions. Microsoft as tools like VCC, Verifast, SLAM, etc to verify C in drivers. I'm curious what combo of them they used on it if any.
  - Matthias247 10y ago
    For me it's a very interesting question whether they directly used the generated C code from the P toolchain in the driver or whether they only used P for verification of the state machines and reimplemented them in C. Directly using the code would be a huge achievement and can help to avoid a lot of issues that will come with reimplementing it. However it has also quite huge requirements for the code generation. E.g. the scheduler must fit the target system and must be performant for the use-case, the infinite-queue semantics that the state machines seem to have are not ideal for a constrained environment and of course there's questions regarding memory allocation and garbage collection (which should mostly be avoided in drivers).

Camillo 10y ago

The README says: "P has been used to implement and validate the USB device driver stack that ships with Microsoft Windows 8 and Windows Phone". It's not clear from your answer. Does Windows ship with a "USB device driver stack" written in P, yes or no?

nickpsecurity 10y ago
The way these normally work is that they do the state machine in the domain-specific language, verify it, auto-generate code in something like C, and compile that. That's almost all of them since it's easy to go from models to code automatically for state machines. The Github page says: "Not only can a P program be compiled into executable code, but it can also be validated using systematic testing. P has been used to implement and validate the USB device driver stack that ships with Microsoft Windows 8 and Windows Phone. " That indicates they modeled it in P with their tool compiling the P specs into some executable. The individual functions the state machine calls would be other C or assembly functions. Microsoft as tools like VCC, Verifast, SLAM, etc to verify C in drivers. I'm curious what combo of them they used on it if any.
- Matthias247 10y ago
  For me it's a very interesting question whether they directly used the generated C code from the P toolchain in the driver or whether they only used P for verification of the state machines and reimplemented them in C. Directly using the code would be a huge achievement and can help to avoid a lot of issues that will come with reimplementing it. However it has also quite huge requirements for the code generation. E.g. the scheduler must fit the target system and must be performant for the use-case, the infinite-queue semantics that the state machines seem to have are not ideal for a constrained environment and of course there's questions regarding memory allocation and garbage collection (which should mostly be avoided in drivers).