И снова про статьи, в этот, раз предлагается посмотреть на статьи про seL4 - формально верифицированное микроядро. (Такая штука, которая работает практически в любом вашем телефоне, а в её гипервизоре уже работает OS, которая видна пользователю).
https://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf - рассматриваются принципы дизайна подобной системы с точки зрения формальной верификации и то какие инструменты используются для этого.
http://sigops.org/sosp/sosp13/papers/p133-elphinstone.pdf - история ядер L4, с концентрацией на технической реализации, реализация IPC, управлением памятью и планировщиком процессов. А так же от каких решений приходилось отказываться и почему.
Не то, чтобы всем приходилось каждый день писать микроядра, но чтение может быть интересным и полезным даже для тех, кто этим не занимается.
https://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf - рассматриваются принципы дизайна подобной системы с точки зрения формальной верификации и то какие инструменты используются для этого.
http://sigops.org/sosp/sosp13/papers/p133-elphinstone.pdf - история ядер L4, с концентрацией на технической реализации, реализация IPC, управлением памятью и планировщиком процессов. А так же от каких решений приходилось отказываться и почему.
Не то, чтобы всем приходилось каждый день писать микроядра, но чтение может быть интересным и полезным даже для тех, кто этим не занимается.
And again about articles, this time, it is proposed to look at articles about seL4 - a formally verified microkernel. (Such a thing that works in almost any of your phones, and the OS that is visible to the user already works in its hypervisor).
https://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf - the design principles of such a system are examined in terms of formal verification and what tools are used for this.
http://sigops.org/sosp/sosp13/papers/p133-elphinstone.pdf - history of L4 cores, with a focus on technical implementation, IPC implementation, memory management and process scheduler. And also what decisions had to be discarded and why.
Not that everyone had to write micronuclei every day, but reading can be interesting and useful even for those who don't.
https://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf - the design principles of such a system are examined in terms of formal verification and what tools are used for this.
http://sigops.org/sosp/sosp13/papers/p133-elphinstone.pdf - history of L4 cores, with a focus on technical implementation, IPC implementation, memory management and process scheduler. And also what decisions had to be discarded and why.
Not that everyone had to write micronuclei every day, but reading can be interesting and useful even for those who don't.
У записи 1 лайков,
0 репостов,
131 просмотров.
0 репостов,
131 просмотров.
Эту запись оставил(а) на своей стене Alexander Vershilov
