Add glossary to manual #1143
Add glossary to manual #1143
Conversation
|
@Indanz Can you pls check over the first draft of the glossary for the seL4 manual? |
|
I assume the glossary us based off the one we have in the abstract spec? I haven't looked through everything yet, but I'd like to before we merge it. It'd be important to get the definitions right, because that's where people will look things up and I don't think we've reviewed the one in the spec very carefully for clarity and precision. Now would be a good opportunity for that. |
It's based on the abstract spec and the current manual. It should definitely be reviewed with a view to getting the definitions exactly right. |
There was a problem hiding this comment.
I'll wait for the update before reviewing the rest.
What are the criteria for adding an entry and where are the descriptions coming from?
E.g. do we want to limit it to seL4 specific things, or should it be broader, like hardware specific things? But then where do we draw the line? It's a seL4 manual, not a general computer architecture manual, so what baseline knowledge should we expect?
Good questions. I'd say, terms that have special meaning for/under seL4 should definitely be there. E.g. "thread" is a general OS term, but we should define what we mean by it in seL4 because there are so many variants of meaning out there (and the current "= CPU abstraction" is probably not enough for that purpose). ASID is also a general term, but seL4 ASIDs are not exactly the hardware ASIDs of the underlying platforms, so that should be defined. Other than that, I'd only include terms if they are obscure and wouldn't expected to be known to a general OS audience. We should be able to assume general OS knowledge, maybe someone with a CS degree, but not specific microkernel knowledge or very detailed computer architecture knowledge. I.e. I don't think we should define things like "scheduler" or similar, but even if ASID didn't have a specific seL4 meaning, we should probably include it, because it's not something people would interact with unless they are implementing a kernel themselves. Of course, things that people would not interact with on the seL4 API level don't need to be in there. The current set of terms and definitions is from a long time ago when we first published the abstract specification, and the target audience was a bit different there -- it was for people who know formal methods, but not so much the OS side, so it's possible that a few of these could be dropped. |
As far as I know seL4's ASIDs are a thin layer on top of the hardware's ASID, just like IRQ objects are. seL4's ASID pools have no functionality other than to keep track of which ASID numbers are used and which are free. There is no generic seL4 ASID code, only arch specific code. The purpose of ASIDs is avoid flushing caches on every context switch, nothing else. I don't think seL4 supports using more ASIDs than the underlaying hardware supports. That is, the current task limit is equal to the hardware's ASID limit, seL4 doesn't do any full cache flushes and dynamic hw ASID assignment. (Edit: The hardware's ASID range is split into multiple pools, so I removed the misguided part.) |
bbrcknl
force-pushed
the
add_glossary_to_manual
branch
from
caef9d8
to
d997c44
Compare
|
Probably not worth considering at this point, given that perhaps the makeindex things seem like they might be sorted in the Makefile now? But perhaps worth mentioning that the latex acro package doesn't require these separate build steps. |
For architecture configurations that don't have a large number of hw ASIDs, seL4 does do dynamic hw ASID assignment. This is at least the case on aarch32 and aarch64 with hyp enabled. |
You are right, I missed that code (I looked at fast path code and misinterpreted the ASID code in there). I understand the need for it on 32-bit ARM, but aarch64 seems unnecessary? ASIDs are still 16-bits there, but for some reason seL4 choses to use VMIDs as ASIDs there? |
(I think we discussed this in another thread already, but just briefly replying again here too.) When aarch64 is running in EL2 as a hypervisor, it only provides stage 2 address space translation from IPA to PA and the TLB tags for these entries use VMIDs which on the currently supported platforms only have 8bits. |
Yes, we did here.
I suspect this is the reason I saw a huge performance drop when going above 256 tasks. Even if tasks are mostly idle, the occasional wakeups flush the L2 cache, degrading system performance badly. I didn't look in detail though, it could have been general cache thrashing too. To use ASIDs for EL0 tasks too, two-stage translation need to be used. That seems to have about 3% overhead, which could be much better than now. However, the seL4 changes for that are quite big and no one else runs that many tasks. Anyway, describing the purpose of the seL4 ASID objects shouldn't be the glossary's goal, however, it should give a short summary that ASID can refer to either HW Adress-Space Identifiers or seL4's object to help managing the hardware ASIDs. |
|
There still seem to be some capitalisation changes in the same commit that adds the glossary and an accidentally committed file |
lsf37
force-pushed
the
add_glossary_to_manual
branch
from
850b94a
to
f4ba907
Compare
manual/parts/glossary.tex
Outdated
|
|
||
| \newglossaryentry{badge}{ | ||
| name=Badge, | ||
| description={A badge is a piece of extra information stored in a capability. It can be used by applications to identify caps previously handed out to clients} |
There was a problem hiding this comment.
| description={A badge is a piece of extra information stored in a capability. It can be used by applications to identify caps previously handed out to clients} | |
| description={A badge is a piece of extra information stored in a capability, mostly used in endpoint and notification capabilities. It can be used by applications to identify caps previously handed out to clients} |
There was a problem hiding this comment.
"with" or "for" seems more appropriate than "in". Otherwise a good improvement. Any other use cases for badges are truly obscure and I can't think of anything useful, other than perhaps limiting further copying or revocation.
There was a problem hiding this comment.
I made the change using:
description={A badge is a piece of extra information stored in a capability, mostly used for endpoint and notification capabilities. It can be used by applications to identify caps previously handed out to clients}
There was a problem hiding this comment.
After the small content changes in the glossary I think this can be merged modulo one last bit: the glossary doesn't have a chapter number, but the bibliography coming after the glossary does, which looks weird in the TOC. If someone knows how to give it a chapter number, we should do that. Otherwise I'd propose to swap the order so that the glossary without number comes last.
I would remove the chapter number from the bibliography instead. That's achieved by removing Unrelated, but somewhat related (and I don't know where else to mention it): The page numbering restarts at chapter 1 for me. So it goes from List of Figures on page 10, to Introduction on page 1. |
I'd be fine with that as well, no specific preference.
That's intended for that style. It basically has a front matter with its own page numbering and then the main text. We can think about if that's really what we want, but it's at least not a bug or oversight :-). Should do that in a separate issue or PR, though. (There is something to be said for page numbers matching up with PDF pages, but there are also arguments for the traditional typesetting way of doing things). |
bbrcknl
force-pushed
the
add_glossary_to_manual
branch
from
9e0fde3
to
c4895d8
Compare
Add a glossary with seL4-specific terms and their definitions. Remove chapter number from bibliography Tweak Makefile for glossary Signed-off-by: Birgit Brecknell <bbrcknl@gmail.com>
bbrcknl
force-pushed
the
add_glossary_to_manual
branch
from
c4895d8
to
373b444
Compare
|
Some hardware tests failed after merging, but all the failures appear to be due to a temporary loss of network connectivity. There were plenty of hardware tests that passed, so I think this is fine. |
|
Yes, that's fine, these connectivity issues seem to be popping up a lot lately. |
manual/parts/io.tex