|
|
|
|
|
|
by naasking
2992 days ago
|
|
|
That might be tough for the Shapiro's argument. The EROS site is no longer available, the mailining lists are no longer available either, and citeseer's google results aren't working at the moment. Shapiro mentions a few issues in this paper which mirror the L34 arguments below [1]. For L4, there's brief mention here of the VFiasco project which attempted a verified L4 using C++, which failed despite considerable effort [2]. [3] is perhaps a better review of what worked and what didn't work in L4 research, and they explicitly discuss the issues, such as the fact that C++ conveyed no real advantages over C, the extra complexity of C++ made verification intractable (even for a subset), and practically, the availability of good C++ compilers for embedded systems was limited. [1] http://webcache.googleusercontent.com/search?q=cache:PQMCrw4... [2] http://web5.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.... [3] https://ts.data61.csiro.au/publications/nicta_full_text/8988... |
|
|