Reading view

There are new articles available, click to refresh the page.

About the Advent of Code category

Advent of Code is a series of daily programming puzzles from December 1st to 25th, becoming progressively more difficult each day.

I’d like to encourage conversation about the problems and solutions in Ada and SPARK on this forum.

I’ve created a new Advent of Code category. If you don’t see a topic for today’s puzzle, feel free to create one. Discussion of general techniques and tools not tied to a specific puzzle is also welcome.

I’ve installed the “Spoiler Alert” plugin, you should use this when posting completed solutions. See below for an example of how to use this feature, along with syntax highlighting.

Screenshot 2022-11-14 19.39.12

1 post - 1 participant

Read full topic

Unusual hardware register behavior

On the RP2040, each GPIO pin can trigger four different interrupts: high level, low level, rising edge, and falling edge. Each pin has a 4-bit field for selecting which of these interrupts is enabled. I modeled it as an array of records.

with System;

procedure Main is
    type INT_Field is record
        Low_Level, High_Level, Falling_Edge, Rising_Edge : Boolean := False;
    end record
        with Size => 4;
    for INT_Field use record
        Low_Level    at 0 range 0 .. 0;
        High_Level   at 0 range 1 .. 1;
        Falling_Edge at 0 range 2 .. 2;
        Rising_Edge  at 0 range 3 .. 3;
    end record;

    type GPIO_Pin is range 0 .. 30;
    type INT_Register is array (GPIO_Pin) of INT_Field
        with Component_Size => 4;

    type GPIO_Peripheral is record
        INTE : INT_Register; --  Write to enable interrupts
        INTS : INT_Register; --  Masked status of enabled interrupts
        INTR : INT_Register; --  Unmasked interrupt status, write to clear
    end record;

    GPIO : GPIO_Peripheral
        with Import, Address => System'To_Address (16#4001_40F0#);
    GPIO.INTE (7).Rising_Edge := True;
end Main;

I’m simplifying things a bit here for clarity. You can find the actual implementation on GitHub

On the surface, this looks like it should work. Compiling with GNAT, this results in a strb (Store Byte) instruction after shifting some bits around.

Now this is where the bug comes in… The RP2040 datasheet explains:

2.1.4. Narrow IO Register Writes

Memory-mapped IO registers on RP2040 ignore the width of bus read/write accesses. They treat all writes as though they were 32 bits in size. This means software can not use byte or halfword writes to modify part of an IO register: any write to an address where the 30 address MSBs match the register address will affect the contents of the entire register.

By “affect the contents of the entire register,” it means that an 8-bit write to a 32-bit register will change all of the bytes of the register to the same value.

If our register value is 16#0000_0000# and the strb instruction is setting bit 8 so that we have 16#0000_0100#, the resulting value is 16#0101_0101# instead.

My solution is to add another array to group fields into 32-bit array elements, so that we can use the Volatile_Full_Access aspect to guarantee that the whole word is written using the str instruction.

    type INT_Register is array (0 .. 7) of INT_Field
        with Volatile_Full_Access, Component_Size => 4, Size => 32;

    type INT_Group is array (0 .. 3) of INT_Register
        with Component_Size => 32;

This solution works, but has left me wondering how we can prevent this from happening again in the future. This is not the first bug I’ve encountered caused by the narrow write behavior of the I/O memory.

I have a few questions for discussion:

  • Is there a way to tell the compiler that a memory range only supports writes of a specific size?
  • If not, can we at least generate a warning?
  • SPARK has the Async_Writers aspect, which indicates that some external process can modify the register value. If we were to verify this code, it seems like every register would need this aspect due to this narrow write behavior.
  • Philosophically, is it possible to make any guarantees about the software without access to the hardware HDL sources? It seems like there’s a bit too much human error possible in the process of writing and interpreting documentation about hardware behavior.

6 posts - 5 participants

Read full topic

Unicode strings

With Ada 2022’s support for user defined type literals, Unicode strings should be easier to work with. I worry that everyone is going to implement their own slightly different string type and we’ll end up with a bunch of incompatible libraries in Alire.

It looks like AdaCore is building VSS (derived from Matreshka) while also maintaining XML/Ada, which has it’s own Unicode package and types.

As a community I think we should define a common interface, or risk spending the rest of our lives converting string representations.

14 posts - 9 participants

Read full topic

Ada library wishlist

I’d like to write more applications in Ada, but I often find that I need a library that doesn’t exist or isn’t well maintained. I thought it might be a good idea to share my wishlist in case anyone is looking for a project or wants to collaborate. I may have already started prototyping some of these.

  • HTTP - I don’t really like AWS and I think something simpler, like Go’s net/http for both clients and servers would be extremely useful.
  • Jinja2 - I have a couple of large Python apps that I’d like to rewrite in Ada, but the lack of a Jinja2 template parser means I’d have to rewrite my templates. I really don’t want to rewrite the templates.
  • Software defined radio - It would be really nice to prototype some wireless protocols using a HackRF. I do have some bindings written for the hardware, but am a bit out of my depth with the complex linear algebra needed to implement the filters. Some real world examples of Ada.Numerics usage would be helpful.
  • Error correction - LDPC and BCH would be nice to have on lossy radio links.
  • RP2040 PIO drivers - I’d love to get the VGA demo board fully working, especially the SD/MMC card interface using all four data lines.
  • Prometheus metrics - A simple library for pushing metrics to Prometheus or similar would be nice. There are even some good notes on client library design in their docs.
  • USB audio drivers - I could really use USB audio class support in the usb_embedded for one of my projects.

What’s on your wishlist?

10 posts - 7 participants

Read full topic