| commit | 5c5ceddf1c76947ee893924f6d59fe836823753a | [log] [tgz] |
|---|---|---|
| author | Andrew Jeffery <andrew@codeconstruct.com.au> | Mon Aug 11 14:45:43 2025 +0930 |
| committer | Andrew Jeffery <andrew@codeconstruct.com.au> | Thu Aug 14 13:49:19 2025 +0930 |
| tree | cbe1e832286dbc7b7a9935da30721d098de94e12 | |
| parent | ad045dd8d9020c4c60804a448eec924b2ed5ba88 [diff] |
CONTRIBUTING: Add "little proofs" article by Matthew Prast
It contains some pretty nice advice, summarized somewhat towards the
end:
- Look for monotonicity and immutability.
- Write code that is monotonic and uses immutable data structures.
- Keep track of your pre- and post-conditions.
- Start with pre- and post-conditions and write your code around
those. Structure your code so that the pre- and post-conditions
are easy to conceptualize and verify.
- You can prove a function maintains an invariant by proving each
unit of work does.
- You should subdivide your code into the smallest possible units
that can maintain the invariant.
- Pay attention to where component boundaries act as "firewalls" that
prevent change propagation.
- Do your best to build as many of these "firewalls" as possible,
and take advantage of them when writing new features.
- Use induction to prove things about recursive functions
incrementally instead of all at once. Assume the inductive hypothesis
is already proved, and use that to your advantage.
- Write your recursive functions incrementally. Assume the recursive
call is already implemented and write the part of the function
that builds the N+1 case from the N case. Then, separately,
implement the base case.
Change-Id: I7d50750567734ddfdfcc85b764b63af0cefa0842
Signed-off-by: Andrew Jeffery <andrew@codeconstruct.com.au>
This is a library which deals with the encoding and decoding of PLDM messages. It should be possible to use this library by projects other than OpenBMC, and hence certain constraints apply to it:
Source files are named according to the PLDM Type, for eg base.[h/c], fru.[h/c], etc.
Given a PLDM command "foo", the library will provide the following API: For the Requester function:
encode_foo_req() - encode a foo request decode_foo_resp() - decode a response to foo
For the Responder function:
decode_foo_req() - decode a foo request encode_foo_resp() - encode a response to foo
The library also provides API to pack and unpack PLDM headers.
libpldm is configured and built using meson. Python's pip or pipx can be used to install a recent version on your machine:
pipx install meson
Once meson is installed:
meson setup build && meson compile -C build
meson test -C build
libpldmComponents of the library ABI[^1] (loosely, functions) are separated into three categories:
[^1]: "library API + compiler ABI = library ABI"
Applications depending on libpldm should aim to only use functions from the stable category. However, this may not always be possible. What to do when required functions fall into the deprecated or testing categories is discussed in CONTRIBUTING.
libpldm is maintained with the expectation that users move between successive releases when upgrading. This constraint allows the library to reintroduce types and functions of the same name in subsequent releases in the knowledge that there are no remaining users of previous definitions. While strategies are employed to avoid breaking existing APIs unnecessarily, the library is still to reach maturity, and we must allow for improvements to be made in the design.