HNHacker News
TopNewBestAskShowJobs

el_pollo_diablo

132 karma · joined November 30, 2023

submissionscomments
el_pollo_diablo··on The science of Monkey Island: can grog dissolve a metal mug that fast?
¡He dejado en libertad los prisioneros y ahora vengo por ti!
el_pollo_diablo··on Intrusive linked lists (2019)
> declared in separate translation units

Now if I include both library headers in code that attempts to plug them together, the types will be incompatible.

Although not a proof in itself, GCC and Clang seem to agree: https://godbolt.org/z/1ocr5Go5b.

el_pollo_diablo··on Intrusive linked lists (2019)
> Taking the pointer to payload[] field is in no way different from doing "(char*) x + offsetof(struct node, payload)"

It may differ, depending on the precise notion of provenance being applicable. If provenance only has allocation granularity, I suppose that there is no difference. I know that there were some discussions about provenance and subobjects. I do not know whether the question is resolved.

Where this gets complicated is that zero-sized arrays are non-standard. So even if we could build a convincing argument from standard notions of provenance, how would it transfer to a subobject that is excluded from the standard?

Last but not least, this is not only about creating the effective type through memcpy. The question is also whether this destroys the effective type of the structure. See my previous point about possible padding after 'payload'.

Please also consider that flexible array members are here for a reason. If I follow your argument, then they bring nothing that arrays of length 0 or 1 do not already cover.

el_pollo_diablo··on Intrusive linked lists (2019)
> how does this work?

Like this:

  struct thread {
      // Entry in the list of threads of the containing process
      list_node process_entry;
      // Entry in this thread's scheduling queue
      list_node sched_entry;
      // ...
  };
Each struct thread is linked in two lists. When we need to get from a list_node * to the enclosing struct thread, we know from the context which list is being inspected, so we know which one of process_entry or sched_entry to consider for offsetting the pointer.
el_pollo_diablo··on Intrusive linked lists (2019)
We mean compatible as defined by the C language standard. It is much more restrictive than having the same layout. In particular, you may not pass a pointer to a type where a pointer to an incompatible type is expected, even if the types have the same layout, which prevents the sort of sharing between two libraries that is being discussed.

Moreover, there is no guarantee that two distinct structure types with the same list of members have the same size or alignment (although in practice they do). The members must nevertheless be laid out in the same way (same offsets, and in the case of bit-fields, same layout inside storage units) due to an obscure constraint on common initial sequences. So the layouts of the structures may differ in the alignment requirement and the amount of trailing padding.

el_pollo_diablo··on Intrusive linked lists (2019)
> The structs list_of_A and list_of_B are compatible.

No, they are not. From C23, 6.7.3.4 Tags: Each declaration of a structure, union, or enumerated type which does not include a tag declares a distinct type.

el_pollo_diablo··on Intrusive linked lists (2019)
> IIRC GCC and Clang lets character types alias to any type.

It is always legal to access the memory representation of any object as an array of characters. The other way around (interpreting an array of characters as a T, even though it does not have effective type T) is not.

> Otherwise glibc’s malloc also doesn’t abide to strict aliasing.

It may not have to. From the point of view of C, malloc is special because it is part of the implementation. The compiler is free to handle UB as it sees fit. In particular, it can decide that aliasing has different semantics in malloc.c than outside it.

el_pollo_diablo··on Intrusive linked lists (2019)
> It does matter, for malloc-returned storage. You can put whatever objects you want into that storage as long as it fits and the pointer is properly aligned.

You can certainly store an object of arbitrary type, but here it is done through a pointer to an object with pointer arithmetic going beyond the allowed bounds.

> memcpy takes a void pointer as its destination, sets the effective type of the storage behind it

And, in doing so, may very well overwrite the unspecified padding following 'payload' in the structure, thus instantly destroying the effective type of the structure object itself. Subsequent accesses to the structure or its members will be UB.

It seems to me that your argument hinges on two assumptions:

    - there is no padding following 'payload' (this would have to be statically asserted),
    - the pointer to 'payload' is indistinguishable from the pointer past the structure; in particular, provenance is not an issue.
That is a very interesting discussion.
el_pollo_diablo··on Intrusive linked lists (2019)
> as long as the struct tags are the same

Exactly. Now you have a naming problem. You need a naming convention that every user of the list library must follow, or else their types will be incompatible. And what about typedefs? If A is a typedef of B, or more generally A and B are typedef-related (their normal forms, obtained by following all typedefs, are the same), lists of A and B will be incompatible unless users agree on a common name. The only realistic choice is the normal form, but then this actively works against the abstraction provided by typedef.

And this is just for types. What about functions? While it is legal to do identical definitions of struct list_int, it is not for list_int_init() and list_int_add(). Or global variables: it is legal to do several identical extern declarations, but there can only be one definition; which compilation unit gets to do it?

el_pollo_diablo··on Intrusive linked lists (2019)
> There is no OoB access of an array

Yes, there is. It does not matter that storage happens to be allocated beyond the end of said array. Strict aliasing implies that it is UB to reinterpret the array as anything else. And it is UB to access an array out of bounds.

Flexible array members specifically exist for these dynamically-allocated trailing arrays. They do not solve the strict aliasing problem, though.

> if the payload type has an alignment that's greater than the size of a pointer

The amount of padding is implementation-defined. The only portable guarantee is that 'payload' is aligned for its element type, char. To over-align, use _Alignas, as in:

    struct node {
        struct node *next;
        _Alignas(max_align_t) char payload[]; // Satisfies all fundamental alignment requirements
    };
el_pollo_diablo··on Intrusive linked lists (2019)
> I do not think a type-safe macro-generated list in C is any more awkward to implement or inferior to a C++ template version.

I have some experience with this, and while this is one of these things that are feasible, I find them significantly inferior to templates in practice.

For one thing, footguns are everywhere in C macro-based metaprogramming. E.g. do not declare the payload as 'payload_type payload;' in the node structure, but choose 'typeof(payload_type) payload;' instead, as someone may pass an array type or function pointer type for 'payload_type'. Speaking of array types, how do you deal with the fact that you cannot pass them by value? I will choose C++ templates' semantic substitution over C macros' textual substitution.

Anyway, to me, the biggest limitation of macro-generation compared to templates is that there is no centralized monomorphization. If an application uses two libraries, each of which handles lists of int, each library will have to independently macro-generate its separate list implementation, and because C's type system is nominal, the generated types will be isomorphic but incompatible. Contrast this with C++ templates, where two independent libraries can happily share std::list<int> values.

el_pollo_diablo··on Intrusive linked lists (2019)
Zero-sized arrays are not standard. Accessing an array out of bounds is UB. At the very least, you should use a flexible array member instead (char payload[];).

But even if you did that, strict aliasing implies that 'payload' can only be accessed as an array of character type. It is correct to memcpy between 'payload' and another object of arbitrary type T of the appropriate size (as list_push_ does in your example), but it is UB to access 'payload' in place as a T (as main does, by casting to struct point * and dereferencing). Oh, and 'payload' may not satisfy the alignment requirement of T.

There is no realistic strict-aliasing-abiding way around a distinct node type per payload type.

el_pollo_diablo··on Intrusive linked lists (2019)
The go a bit further than the article on the advantages of intrusive data structures, taking linked lists as an example:

As the article mentions, intrusive data structures naturally lead to one fewer indirection. To do the same with a traditional list (where the list node owns the payload), a different node type is needed for each payload type. This is easy to do with the proper support for monomorphized generics, see C++'s std::list. It is awkward in C, where the implementation has to be macro-generated. C naturally pushes towards an indirection through void *, which makes intrusive lists more attractive.

One other advantage of intrusive data structures is the ability to link a payload into several parallel collections without indirections (where traditional collections would require e.g. one collection owning the payloads, and the other collections merely holding non-owning pointers to them).

Las but not least, the defining property of intrusive data structures is that they leave the responsibility of allocating the elements to the user. The elements can be allocated on the heap, on the stack, in a global array (like "initholes" in the article), in a special arena, etc. It is even reasonable to use non-uniform allocation strategies; for example, for a circular list, allocate an anchor node on the stack and the other nodes (those embedded in payloads) on the heap.

el_pollo_diablo··on We have proof automation now
> a single proof covering the most precise description of the program's behavior is more compact

Yes, and a program is most compact when all modules have been merged, and all functions with a single caller inlined. We have compilers with LTO for that, though; we would never maintain source code in that form.

Snark aside, I get your point about restating the program code, but this can be alleviated by interactive proof assistants that largely reduce the length of proof scripts. This is mostly a matter of tooling.

el_pollo_diablo··on We have proof automation now
In my view, a major selling point of dependent types when it comes to reasoning, is that by bundling logical properties with a runtime value, they require no separate effort to prove the propagation of the logical properties as the value is moved around. That is why I mentioned them in the context of opaque types. This is especially useful with generics: when a type parameter is instantiated with a dependent type, all its occurrences instantly benefit from the strong typing.

They can also be used to enforce just enough constraints on the inputs of a function to make it total, but this comes down to the tradeoff between either leaving an error path in the program and proving its unreachability later, or not having this error path but immediately requiring the proof. In any case, as you mention, further properties can be proved later without altering the dependent type.

I do not intend to come off as overly negative about dependent types. They have their uses, but they can also bring a maintenance nightmare.

el_pollo_diablo··on We have proof automation now
I am not sure what you mean. Of course proving a new property generally implies reasoning on each elementary step of the program. My point is that, assuming you have already proved a property, proving a new one shouldn't lead you to alter the first proof. But it does if you carelessly use some logical tools like dependent types and single preconditions/postconditions/loop invariants.

For example, take Hoare's while rule (see https://en.wikipedia.org/wiki/Hoare_logic#While_rule). If you have already proved

    {P∧B}S{P}
and, in order to prove another property, some new invariant Q has to be propagated across this loop. It would be enough to prove

    {Q∧B}S{Q}
or even

    {P∧Q∧B}S{Q}
if the new proof builds upon the first one. But if your logical tool of choice insists on having a unique loop invariant, you must throw away your existing proof and prove

    {P∧Q∧B}S{P∧Q}
which is incomparable and uselessly mixes both concerns.
el_pollo_diablo··on We have proof automation now
I have already written it, and I will write it again: dependent types and total functions do not scale. Maintenance is terrible.

Suppose that you have managed to write a non-trivial piece of software with dependent types encoding all sorts of properties everywhere. The actual computation and proof are intermingled. Think of the author's innocent bound-check proof in the zstd decoder, but across the whole program, with more elaborate properties and longer proofs.

Suddenly, you realize that you need to prove a new property of your program. Can you keep your existing work and build on top of it? In general, no, you have to refine every dependent type everywhere by adding a new conjunct expressing a new invariant, and adapt every proof, as the new property is threaded in the existing program.

That is because dependent types (and other staples of naive approaches to proving program properties, like a unique invariant per loop) structure the program along the wrong dimension: they encourage grouping everything that concerns a value ("put this value in a dependent type that encodes everything known about it") or a program point ("write the precondition for this function as a big conjunction mixing all the concerns"), where it works much better, for long-term maintenance, to structure the development along concerns: computational parts of the program, basic functional properties and absence of UB, termination, other functional properties, security, etc., where each layer builds on top of the previous ones without requiring them to change.

That is not to say that dependent types do not have their use. Where they shine is at module boundaries. Consider a library that exposes an opaque type and operations on it. Users of the library can only build and modify values of that type through the library's API. This type should be a dependent type. If it needs to be refined at any point to encode a new invariant, this will have no impact on the library's users, since all they do is pass around values without interpreting them. However, inside the library, I would recommend unpacking/repacking the dependent type at the library's entry points and handling the concerns separately.

el_pollo_diablo··on Everything in C is undefined behavior
> probably meaning on an address that’s a multiple of sizeof(int), but who knows

Sigh. s/sizeof(int)/_Alignof(int)/.

There are good reasons for an implementation to have sizeof(int) = _Alignof(int) and not a mere multiple of it, but if you are going to discuss subtle points and UB, just stick to the language guarantees.

> But let’s say you have a modern machine, where NULL is a pointer to address zero, and you actually have an object there.

You don't program in C on such a machine. Or maybe memory is virtualized, and it does not matter that your object lives at physical address zero, as long as you can map a non-zero virtual address to it.

> So how do you print an uid_t?

    if ((uid_t)-1 < (uid_t)0) {
        // uid_t is signed
        printf("%" PRIdMAX, (intmax_t)id);
    } else {
        // uid_t is unsigned
        printf("%" PRIuMAX, (uintmax_t)id);
    }
> It’s not rare for the denominator to come from untrusted input.

It's not rare for the array index to come from untrusted input.

It's not rare for the supposedly valid UTF-8 string to come from untrusted input.

...

Why single out division? This problem affects every partially defined operation. In the case of division at least, everyone learned in school that thou shalt not divide by zero. Adding two untrusted integers and forgetting that signed overflow is UB, not defined as a modulo? Your average programmer is much less likely to see that coming.

    > unsigned char a = 0xff;
    > unsigned char b = 1;
    > unsigned char zero = 0;
    > bool overflowed = (a + b) == zero;
    >
    > unsigned char a = 0x80;
    > uint64_t b = a << 24;
Please. Convert your operands to wide enough types before the operation. Convert your results back to narrow enough types to compensate for integer promotion to wider types than you would have liked. Do that consistently, and you're good.

Here:

    unsigned char a = 0xff;
    unsigned char b = 1;
    unsigned char zero = 0;
    bool overflowed = (unsigned char)(a + b) == zero;

    unsigned char a = 0x80;
    uint64_t b = (uint32_t)a << 24;
el_pollo_diablo··on Int a = 5; a = a++ + ++a; a =? (2011)
Type punning via unions is not UB in C in general, but it is in C++ IIRC.

I write "in general" because, as with other forms of memory reinterpretation (memcpy or copy through a character type), evaluating a trap representation triggers UB.

el_pollo_diablo··on Box to save memory in Rust
So there are now two ways to represent the same state: None or Some(struct whose fields are all None). Even though one of these representations is never produced by the deserialization routine, anyone could construct it if the constructor is public. And even if they don't, the different representations will show up in pattern matching as separate paths for every access to the field. This looks like a good opportunity to make these types (optimized for storage) private, and to define public view objects/accessors (optimized for usage) on top of them that merge equivalent representations.
el_pollo_diablo··on The pleasures of poor product design
This reminds me of Jacques Carelman's Catalogue d'objets introuvables. Highly recommended. It has already been mentioned on HN: https://news.ycombinator.com/item?id=9789216
el_pollo_diablo··on AI will make formal verification go mainstream
Capturing invariants in the type system is a two-edged sword.

At one end of the spectrum, the weakest type systems limit the ability of an IDE to do basic maintenance tasks (e.g. refactoring).

At the other end of the spectrum, dependent type and especially sigma types capture arbitrary properties that can be expressed in the logic. But then constructing values in such types requires providing proofs of these properties, and the code and proofs are inextricably mixed in an unmaintainable mess. This does not scale well: you cannot easily add a new proof on top of existing self-sufficient code without temporarily breaking it.

Like other engineering domains, proof engineering has tradeoffs that require expertise to navigate.

el_pollo_diablo··on Rouille – Rust Programming, in French
Years ago the research team behind OCaml released Chamelle, a version of the language localized in French, as an April fool's joke:

https://gallium.inria.fr/blog/ocaml-5/

el_pollo_diablo··on Greenland’s national telco, Tusass, signs new agreement with Eutelsat
I would put the emphasis on a different word:

> This article is made and published by Anna Hartz, which may have used AI in the preparation

Which, not who. They're not even sure the author is human!

el_pollo_diablo··on I write type-safe generic data structures in C
Head and tail make sense for persistent lists in functional languages with value semantics, yes.

The intrusive, mutable, doubly-linked loops with reference semantics under discussion are quite different. Although all entries behave identically in the structure itself, one of them is _used_ differently, as a standalone anchor point, while the others are embedded in the list's "elements".

el_pollo_diablo··on I write type-safe generic data structures in C
> Are you saying the only real way to program is with generic data structures?

Certainly not. As I said, the experienced programmer knows when (not) to use them. Some programs are better off without them, such as... most of the low-level software I write (security-critical operating systems).

> Data tends to follow a particular path and there is probably 1 red black tree and it’s a core feature of the application. If that’s true then it’s not a big deal to write that core feature of your application.

"It's not a big deal" are famous last words. Maybe it is not a big deal, but unless you have hard constraints or measurements that confirm that you would not be served well enough by an existing solution, it may very well be the reason why your competitors make progress while you are busy reinventing, debugging, maintaining, and obtaining certification for a wheel whose impact you overestimated.

> It avoids premature optimization and code bloat because you tend to use complex data structures when they have a need.

Avoiding code bloat? Agreed, a custom solution cannot be worse than a generic one. Avoiding premature optimization? Quite the contrary: going straight for the custom solution without first confirming, with actual measurements, that the generic solution is the unacceptable bottleneck, is textbook premature optimization.

I am sorry but I do not understand what you are getting at.

el_pollo_diablo··on I write type-safe generic data structures in C
You mean the downside that we also already know, i.e. that there are some situations where a custom data structure would be superior for various reasons (e.g. smaller footprint)?

Experienced programmers know when to reuse a generic library and when to roll out their own. We all know that.

Yet you dismiss generic red black trees because there is no realistic single program that uses 10 key/value combinations. Not only is this false, but as I illustrated in my reply, a single program is not the relevant scope to decide whether to use a generic implementation. And as someone who has written a red black tree library, I am definitely in favor of reusing an implementation unless you have an excellent reason, which "I do not need 10 different instances in my program" or "my favorite language and its standard library only have arrays built in" most definitely are not.

el_pollo_diablo··on I write type-safe generic data structures in C
Absolutely. Wrapping the distinguished entry point in a new structure type equipped with a thin type-safe wrapper API that covers the most common use case is the way to go.
el_pollo_diablo··on I write type-safe generic data structures in C
Not to mention that they insist on calling every entry of the list a "list head", which makes no sense (hysterical raisins, maybe?). The structure is made of a uniform loop of entries, one of which is used as the actual head & tail, or entry point into the structure.
el_pollo_diablo··on I write type-safe generic data structures in C
None, but that is not my point. Before C23, fn() already meant the same thing as fn(void) in function definitions, which the situation under discussion here.

C23 changed what fn() means outside a function definition.

Page 1 of 2Next →