reserved identifier violation about sel4 HOT 18 CLOSED

I think that for the API headers it may be reasonable to have the __ prefix. I think that in practise __ is not a problem for most programs and so the __ prefixes aren't really a problem. One thing I would suggest is to have a SEL4 prefix for the header guards (especially for the API headers). In practise __SEL4_API_H would not be a problem but I could easily imagine __API_H being a problem.

from sel4.

How do you think about to avoid that this software depends on undefined behaviour?

from sel4.

Note that these are C preprocessor directives used for conditional header inclusion, not C identifiers. The actual C compiler never sees them. Nevertheless, in normal C code you should avoid them, because they are reserved for the compiler and C runtime system (such as libc), and might already be taken. We are implementing part of that runtime environment here, though, so these names are appropriate in this case.

Also note that there are some real instances in the kernel that according to the C standard are undefined behaviour. For instance, implementing the first layer of any memory allocation has to use undefined behaviour, because it has to access memory that has not been allocated yet. This is nothing special, any low-level OS kernel or library that implements malloc has to do something like this.

The difference in seL4 is that we can validate that the compiler still produces the expected correct code, even though it would be free to do otherwise according to the C standard. This is what the binary proof phase is good for.

This implies something pretty cool: we don't have to care whether the code violates the C standard or not. We can prove that it works anyway, even if it does. In reality, we are sticking to the standard very closely, though.

In terms of having a SEL4 prefix: these headers are kernel-only code, not supposed to be included from anywhere else (i.e. they are not headers that user code would include). If that is violated, the earlier it clashes and gets noticed, the better. The story is different for user headers. See for instance libseL4 for that, which does have such a prefix.

from sel4.

Preprocessor symbols are also identifiers. Are you going to delete some underscores from them which do not belong to the implementation of a compiler for the programming language "C" or "C++"?

from sel4.

"Markus" == Markus Elfring [email protected] writes:

Markus> Are you going to delete some undercores from them
Markus> which do not belong to the implementation of a
Markus> compiler for the programming language "C" or "C++"?

Check the C99 rationale, section 7.1.3: names beginning with double
underscore are reserved for library implementors.
The ones you've been noticing are part of the library implementations
for systems built on seL4.

It says:
Also reserved for the implementor are all external identifiers
beginning with an underscore, and all other identifiers beginning
with an underscore followed by a capital letter or an underscore.
This gives a name space for writing the numerous behind-the-scenes
non-external macros and functions a library needs to do its job
properly.

Dr Peter Chubb peter.chubb AT nicta.com.au
http://www.ssrg.nicta.com.au Software Systems Research Group/NICTA

from sel4.

To put it more strongly, while identifiers such as __API_H are a violation in normal code, on the kernel and system library level they are a) compliant, and b) appropriate. For seL4, they are also c) provably safe.

So, no we don't see a reason to change them, and it would in fact be detrimental because it would suggest to the programmer that she is working in a normal C environment, when that is not the case.

Your sentence part

which do not belong to the implementation of a compiler for the programming language "C" or "C++"?

seems to imply that they would be Ok for a compiler implementation. Note that they are arguably not Ok there. The compiler implementation is not a library, and the underscore identifiers should occur in the names the compiler presents to the programs it compiles, not in the implementation of the compiler itself. (Of course, there is no good reason to even implement a C compiler in C, there are much better languages for that. But that is a different topic).

from sel4.

I try to clarify this detail a bit more:

• Does any component of the software "seL4" belong to a C/C++ compiler implementation (which provides also its own libraries)?
• Would you like to improve standard compliance for your source files?

from sel4.

Yes, of course all components of the seL4 kernel belong to the software stack that implement C/C++ compiler runtimes (or any other language runtime on the seL4 platform). So do the other repositories under the github org seL4/. It's a microkernel, it provides runtime infrastucture.

The source files are already standard compliant.

from sel4.

I see your runtime infrastructure separate from a C/C++ compiler implementation (which can be built on top of that). I suggest to avoid to tamper with the reserved name space at various source code places.

from sel4.

It has to be built on top, that's the entire problem: in C, the preprocessor name space is not separate. If you take the libsel4 headers for instance, they will be an include of any C library and runtime environment the system provides (e.g. libsel4muslcsys, libmuslc, libplatsupport, etc). That's the point of the reserved name space: so you can implement such libraries without clashing with user code. User code on the other hand can assume that as long as it sticks to non-reserved names, it will not clash with any system library names.

If we were to change to non-underscore names, we would break that. That's what Peter was trying to say pointing at the C99 rationale, section 7.1.3.

This is completely standard usage. If you look at gnulibc, it does exactly the same thing, it just isn't decomposed into as many separate components and repositories.

from sel4.

I dare to distinguish more on consequences between name selection in libraries for C/C++ compiler implementations and other software components. Do we need to clarify the different interpretation of the section "7.1.3 Reserved identifiers" from the standard specification by additional communication means?

from sel4.

elfring, do you have any meaningful argument for why the identifiers should be changed? Other people clearly explained why the naming is the way it is. It seems to me you are unable to provide any counterargument, instead being insistent that the literal wording of the standard is honored (as opposed to its intention). That is not productive.

from sel4.

I try to point out my interpretation "seL4 software (including its libraries) does not belong to a C/C++ compiler implementation." as a counter-argument.

from sel4.

@lsf37 and @wom-bat have quoted the relevant sections of the standard and explained how we are compliant and why any deviation is proved safe. Should this issue be closed?

from sel4.

Would you like to clarify such implementation details in an other forum a bit more?

from sel4.

On 5 Aug 2014, at 20:58 , Markus Elfring [email protected] wrote:

Would you like to clarify such implementation details in an other forum a bit more?

The point was clearly made: the use of reserved identifiers in seL4 headers is compliant with the wording and intent of the standard, and is clearly not a violation. I can put you in contact with a member of JTC1/SC22/WG14 if you want to discuss this with them. I don’t see a point of discussing that issue further on this list.

Gernot

from sel4.

@gernotheiser : Thanks for your contact offer. I imagine that another small dialogue might become constructive.

from sel4.

Looks like the discussion is closed, we're happy to continue in another forum.

from sel4.