AHXproject

pedit COW kernel local privilege escalation vulnerability mitigations

Mitigations are available for the Linux vulnerability with CVE ID CVE-2026-46331 . The CVE ID was assigned on June 16 2026 and highlighted as a local privilege escalation (LPE) vulnerability on June 26, 2026. Known as "pedit COW", this vulnerability affects multiple Linux distributions, including all Ubuntu releases starting with Bionic Beaver 18.04 LTS. Ubuntu Resolute Raccoon 26.04 LTS has AppArmor mitigations that block the execution path of the vulnerability.

The vulnerability was assigned a CVSS 3.1 score of 7.8, corresponding to a severity of HIGH, on June 28, 2026.

The affected component is a Linux kernel module that provides support for tc-pedit , an action used by the traffic control  subsystem in Linux that allows for arbitrary packet modification.

This post describes mitigations that disable the affected modules, if they are not needed by a host. These mitigations can be applied until Linux kernel packages which implement the proposed patch are released.

Impact
Deployments without container workloads

On hosts that do not run container workloads, the vulnerability allows a local user to elevate privileges to the root user. There is a published exploit that executes in this type of deployment.

Container deployments

In container deployments that may execute arbitrary third-party workloads, the vulnerability may additionally facilitate container escape scenarios, in addition to local privilege escalation on the host. A proof-of-concept exploit has not been published yet for container escape.

Mitigation regression risk

The mitigation disables the kernel modules that are used for the pedit action in tc. Enabling the mitigation will affect functionality if the module is in use by local traffic control rules.

Affected releases

Once available, the vulnerability fix will be distributed through the Linux kernel image packages. In the interim, a mitigation which disables the affected modules can be applied according to the instructions below. The mitigation will not be necessary once the kernel is updated.

ReleasePackage NameRemediation StatusTrusty Tahr (14.04 LTS)linuxNot affectedXenial Xerus (16.04 LTS)linuxNot affectedBionic Beaver (18.04 LTS)linuxAffectedFocal Fossa (20.04 LTS)linuxAffectedJammy Jellyfish (22.04 LTS)linuxAffectedNoble Numbat (24.04 LTS)linuxAffectedQuesting Quokka (25.10)linuxAffectedResolute Raccoon (26.04 LTS)linuxAppArmor mitigations
How to check if you are impacted

Run the following command to obtain the name of the Ubuntu release installed and compare to the table above:

lsb_release -a
Manual mitigation

The mitigations block the affected kernel module from loading. This requires three steps:

• Prevent the module from loading in the future.
• Unload the module.
• Check whether step 2 was successful; if not, reboot the system.

Step 1 – block the module:

Block the module by creating a /etc/modprobe.d/pedit-cow.conf file:

echo "install act_pedit /bin/false" | sudo tee /etc/modprobe.d/pedit-cow.conf

Regenerate the initramfs images, to prevent the module from being loaded during early boot:

sudo update-initramfs -u -k all
Step 2 – unload module:

Unload the module, in case it is already loaded:

sudo rmmod act_pedit 2>/dev/null 
Step 3 – confirm the module isn't loaded:

Check whether the module is still loaded:

grep -qE '^act_pedit ' /proc/modules && echo "Affected module is loaded" || echo "Affected module is NOT loaded"

If the previous action indicates that the module is not loaded, no further action is required. However, unloading the module may not be possible if it is in use by existing traffic control rules. In these instances, a system reboot will enforce its blocking, but will affect traffic control rules:

sudo reboot
Disabling the mitigation

Once kernel updates are available and installed, the mitigation can be removed:

sudo rm /etc/modprobe.d/pedit-cow.conf
sudo update-initramfs -u -k all

Mitigations are available for the Linux vulnerability with CVE ID CVE-2026-46331. The CVE ID was assigned on June 16 2026 and highlighted as a local privilege escalation (LPE) vulnerability on June 26, 2026. Known as "pedit COW", this vulnerability affects multiple Linux distributions, including all Ubuntu releases starting with Bionic Beaver 18.04 LTS. Ubuntu Resolute [...]


Categories: Security, Vulnerabilities
Source: https://ubuntu.com//blog/pedit-cow-linux-vulnerability-fixes-available Jul 01, 2026, 10:50 AM

Canonical becomes Gold Sponsor of Trifecta Tech Foundation

Canonical is pleased to announce it is now a Gold Sponsor of the Trifecta Tech Foundation , a non-profit that creates open source building blocks for critical infrastructure software. 

Canonical has supported the foundation's work since 2025, co-sponsoring the development of projects like sudo-rs . The new €40,000/year contribution will help the foundation continue developing and maintaining memory-safe system utilities written in the Rust programming language.

"We're grateful to Canonical for stepping up in a big way to support our mission. Maintenance of critical infrastructure software is notoriously difficult to fund, yet it's essential work. Our Gold and Silver sponsors provide flexible, undirected support that makes this possible. This enables us to guarantee the long-term security and reliability of the projects in our Data compression, Time synchronization, and Privilege boundary initiatives."

– Erik Jonkers, Chair of Trifecta Tech Foundation

The next phase in the collaboration will focus on the adoption  of ntpd-rs as the default time synchronization client and server in Ubuntu. Canonical aims to introduce ntpd-rs for testing in Ubuntu 26.10, making it a default in Ubuntu 27.04. With support from the Trifecta Tech Foundation, the transition will deliver gpsd IP socket support, multi-threading support for NTP servers, support for multi-homed servers, and robust AppArmor and seccomp profiles for ntpd-rs. The work Canonical is funding will also deliver support for gPTP (Generalized Precision Time Protocol), which is ideal for deployments in connected vehicles.  

"Increasing memory safety in Ubuntu is a critical part of improving the resilience of devices, servers and PCs worldwide. The adoption of sudo-rs by default in Ubuntu 26.04 LTS signaled a shift from "experimental feature" to "new security baseline" for memory safety. I'm delighted to be supporting the Trifecta Tech Foundation to continue the leadership of memory-safe alternatives to critical software for the benefit of the open source community."

– Jon Seager, VP Engineering, Ubuntu

Learn more about our work to adopt Rust-based system utilities  in Ubuntu. 

About Canonical

Canonical, the publisher of Ubuntu, provides open source security, support, and services. Its portfolio covers critical systems, from the smallest devices to the largest clouds, from the kernel to containers, from databases to AI. With customers that include top tech brands, emerging startups, governments, and home users, Canonical delivers trusted open source for everyone.

Learn more at https://canonical.com/  

Canonical is pleased to announce it is now a Gold Sponsor of the Trifecta Tech Foundation, a non-profit that creates open source building blocks for critical infrastructure software.  Canonical has supported the foundation's work since 2025, co-sponsoring the development of projects like sudo-rs. The new €40,000/year contribution will help the foundation continue developing and maintaining [...]


Categories: Community, Open source, Ubuntu
Source: https://ubuntu.com//blog/canonical-becomes-gold-sponsor-of-trifecta-tech-foundation Jun 30, 2026, 03:04 PM

Challenges designers face in open source (and how to fix them)

Open source software (OSS) is a cornerstone of modern technology. According to the Linux Foundation , it powers up to 90% of software tools used today. Unlike proprietary software, OSS is developed collaboratively, meaning its code is available for anyone to use, change, and distribute.  

Because OSS projects have historically been driven by developers, they tend to be highly flexible and functional, but they can lack critical usability considerations. This often makes them difficult for everyday users to navigate and adopt. To bridge this gap, there is a need for more designers to contribute to open source and improve user experiences.  

With this in mind, Canonical's Design team conducted a survey exploring the real-world experiences of people contributing design work to open source projects. We received 115 responses from a diverse group: UX/UI designers, graphic designers, accessibility specialists, researchers, and design system experts, as well as open source maintainers who work with designers. We followed this up with qualitative interviews with 11 participants from around the world, ranging from OSS newcomers to veterans with over a decade of experience.  

While our full research report will be published soon, we wanted to share some key insights. Here are four primary challenges that designers face in the open source ecosystem, and how communities can address them. 

1. Finding OSS projects that accept design contributions is difficult


OSS design survey: What prevents you from contributing design to OSS projects?

The challenges receiving the most mention from our respondents were visibility and awareness. Many designers are unfamiliar with OSS so simply do not know where to look for projects. Even those who are familiar with open source still struggle to find projects that welcome non-code contributions.

A major factor contributing to this issue is confidence. While project maintainers are experienced in requesting code contributions, many admit they are less confident about requesting design work. Some are unsure how to structure the design contribution request or effectively engage with creative communities.

Initiatives likeOpen Source Design  andContribute.design  are doing an excellent job of curating design-related contribution requests. However, there is still a lot that can be done to increase OSS awareness among designers, and to help maintainers use these platforms effectively.

2. Onboarding and documentation don't support designers

Many OSS projects lack clear documentation for design contributions. While they often feature robust onboarding materials for developers, there is typically little to no guidance for designers.

This gap is partly due to a lack of design awareness among maintainers. 53% of those surveyed admitted they don't understand how design fits into their project, leaving them struggling to document a design contribution workflow.

Without this infrastructure, designers lack critical project context. They may not know the target audience, scope of work, brand guidelines, or technical constraints. This makes starting a project stressful, and many give up before making their first meaningful contribution.

However, some communities are successfully tackling this issue. Projects likeBitcoin Design  andLayer5  attract and retain non-code contributors by implementing proactive strategies like:

• Publishing dedicated "Get Started" guides for designers.
• Establishing structured mentorship systems for new contributors.
• Hosting regular AMA (Ask Me Anything) sessions and community syncs.
• Maintaining transparent design documentation logs.

Layer 5' mentorship program for new contributors

This lowers the barrier to entry and creates a genuinely welcoming environment. At Canonical, we have created a contribution brief template  to give maintainers a clear framework for the information designers might need before they begin contributing.

3. Contribution platforms have steep learning curves

Open source collaboration primarily happens on Git-based platforms like GitHub, GitLab and Launchpad. While these tools are second nature to developers, they are rarely used by designers. New OSS designers frequently find it difficult to navigate issues, pull requests, repositories, and version control workflows. 

The technical nature of these platforms acts as a significant barrier that might deter talented visual and UX contributors from getting involved.

This is another area where better onboarding materials make a massive difference. Beginner-friendly guides can demystify these platforms and simplify workflow setup. At Canonical, we have started addressing this hurdle by creating educational resources, like our recent  video tutorial.

4. Designers face more pushback on non-visual contributions

One of the more surprising findings was that designers face significantly more friction when making non-visual contributions. Over the last decade, digital design has matured from just traditional "visual work" into research, product strategy, information architecture, specification writing, accessibility audits, and more. 

However, designers reported getting a lot more pushback when trying to contribute in these non-visual areas. They frequently have to spend extra time justifying methods and defending fundamental UX decisions to maintainers. 

OSS communities can address this by educating maintainers on the holistic role of design in software development. Additionally, maintainers can provide guidelines on how they review and accept non-code contributions. This transforms feedback into a more objective, structured, and transparent process.

The path forward

Overcoming these barriers requires a collaborative effort from both designers and OSS maintainers:

• Designers can bring immense value to OSS projects by improving accessibility and usability, but need to remain patient with an evolving ecosystem. 
• Maintainers need to find clearer ways to signal openings for design, improve non-code onboarding, and formally recognize the value non-code contributors bring.

Fortunately, pioneering communities are already proving that design-friendly onboarding, structured documentation, and active mentorship works. By adopting these strategies, more OSS projects can attract and retain design talent, ultimately making open source software more inclusive, user-friendly, and widely adopted.

Keep an eye on our blog for the full research report, dropping in the coming weeks!

Join the Canonical design team

We're looking for designers who care about craft and how systems work under the hood. At Canonical, design sits at the intersection of UX, engineering, and open source where we shape cohesive, accessible experiences across cloud, desktop, and IoT products.

If you enjoy solving complex problems and turning technical depth into clarity, explore our open roles: canonical.com/careers

Open source powers up to 90% of modern software, yet many projects lack usability. Canonical's Design team surveyed 115 cross-functional professionals to uncover the 4 core challenges UI/UX designers face when contributing, and how maintainers can solve them.


Categories: Design, open design, Open source
Source: https://ubuntu.com//blog/challenges-designers-face-in-open-source-and-how-to-fix-them Jun 26, 2026, 02:02 PM

Hunting a 16-year-old SQLite bug with TLA+: is dqlite affected?

This article was written by Marco Manino and Alberto Carretero, dqlite team at Canonical.

1. Anatomy of a SQLite bug

Recently SQLite published a new version  with a fix to a long-standing bug  in the way that the Write Ahead Log (WAL) is checkpointed that leads to the corruption of the database.

The important aspect of this bug is not its real-world impact (which is very low) but how long it has been in the repository, how difficult it was to find it, and how difficult it was to reproduce it. Indeed the bug has been present since 2010, for 16 years! Also, the crucial question for us, the dqlite team, is: can dqlite be affected by this?

In order to find out, we first need to be able to understand the exact sequence of steps that leads to database corruption. To do that, we will be using TLA+ to model SQLite's behavior and quickly find a trace that allows us to reason about the bug. Then, we will create a different model that describes how dqlite uses sqlite and we will check whether the bug can happen.

2. Small introduction to WAL and checkpoints in SQLite

SQLite uses WAL mode to allow readers to not be blocked by writers. The way it achieves that is by writing to a special staging area called the Write Ahead Log (WAL). Writers can append to the end of the WAL and readers can ignore the new data until it is stable. Eventually, the staging area is moved to the database; this is called a checkpoint. To prevent the WAL from growing indefinitely, a writer will attempt to "reset" it – i.e. overwriting it – if the previous checkpoint was able to move all the pages. If you are curious to learn more you can find a very clear description in the official documentation .

SQLite orchestrates changes to the WAL using locks and shared memory. For our use-case it is enough to think about writing and checkpointing; as such, we only care about two locks:

• The checkpoint lock (CKPT_LOCK) which is taken before running a checkpoint to prevent multiple from happening at the same time
• The write lock (WRITE_LOCK) which is taken before appending new pages to the WAL

The shared memory contains information needed to orchestrate writers, checkpointers, and readers, together with a data structure to index pages in the WAL for read performance. As we said, readers are not involved; as such, the only interesting fields are:

• walSalt which contains a counter that is incremented each time the WAL is reset
• mxFrame which contains the length of the WAL
• nBackfill which contains the amount of pages that have been already checkpointed, that is, [nBackfill+1, mxFrame] has not been copied to the database at this point

3. Modeling the bug in TLA+

Part of the difficulty of writing TLA+ is deciding what to model and what not to model. We would like to come up with the simplest possible spec that is still faithful to reality and which we can use to extract useful insights from the model.

The first thing to model is our database and WAL as described in the previous section:

\* files.
VARIABLE wal
VARIABLE db

\* wal-index variables:
VARIABLE nBackfill
VARIABLE mxFrame
\* We will only capture the sequential part of the salt.
VARIABLE walSalt

Init ≜
\* wal and db are initially empty.
∧ wal = ⟨⟩
∧ db = {}
∧ nBackfill = 0
∧ mxFrame = 0
∧ walSalt = 0

Since generating the data is out of the scope of the model, we can take a simpler approach. We can model each page of data as a single unique number, then the WAL can be a sequence of such numbers and the database a set of them. In particular, checkpointing will move pages from the sequence in the WAL to the set of the database in the order they were appended to the WAL. To generate a unique number it is enough to use an always increasing counter.

We need to model the two actions that interact and produce the bug: appending and checkpointing. Let's start by looking at the C code in SQLite that appends pages to the WAL to define our TLA+ action:

SQLite code responsible for appending frames to the WAL
static int walFrames(
Wal *pWal, /* Wal handle to write to */
int szPage, /* Database page-size in bytes */
PgHdr *pList, /* List of dirty pages to write */
Pgno nTruncate, /* Database size after this commit */
int isCommit, /* True if this is a commit */
int sync_flags /* Flags to pass to OsSync() (or 0) */
){
int rc; /* Used to catch return codes */
u32 iFrame; /* Next frame address */
PgHdr *p; /* Iterator to run through pList with. */
PgHdr *pLast = 0; /* Last frame in list */
int nExtra = 0; /* Number of extra copies of last page */
int szFrame; /* The size of a single frame */
i64 iOffset; /* Next byte to write in WAL file */
WalWriter w; /* The writer */
u32 iFirst = 0; /* First frame that may be overwritten */
WalIndexHdr *pLive; /* Pointer to shared header */

assert( pList );
assert( pWal->writeLock );

/* If this frame set completes a transaction, then nTruncate>0. If
** nTruncate==0 then this frame set does not complete the transaction. */
assert( (isCommit!=0)==(nTruncate!=0) );

#if defined(SQLITE_TEST) && defined(SQLITE_DEBUG)
{ int cnt; for(cnt=0, p=pList; p; p=p->pDirty, cnt++){}
WALTRACE(("WAL%p: frame write begin. %d frames. mxFrame=%d. %s\n",
pWal, cnt, pWal->hdr.mxFrame, isCommit ? "Commit" : "Spill"));
}
#endif

pLive = (WalIndexHdr*)walIndexHdr(pWal);
if( memcmp(&pWal->hdr, (void *)pLive, sizeof(WalIndexHdr))!=0 ){
iFirst = pLive->mxFrame+1;
}

/* See if it is possible to write these frames into the start of the
** log file, instead of appending to it at pWal->hdr.mxFrame.
*/
if( SQLITE_OK!=(rc = walRestartLog(pWal)) ){
return rc;
}

/* If this is the first frame written into the log, write the WAL
** header to the start of the WAL file. See comments at the top of
** this source file for a description of the WAL header format.
*/
iFrame = pWal->hdr.mxFrame;
if( iFrame==0 ){
u8 aWalHdr[WAL_HDRSIZE]; /* Buffer to assemble wal-header in */
u32 aCksum[2]; /* Checksum for wal-header */

sqlite3Put4byte(&aWalHdr[0], (WAL_MAGIC | SQLITE_BIGENDIAN));
sqlite3Put4byte(&aWalHdr[4], WAL_MAX_VERSION);
sqlite3Put4byte(&aWalHdr[8], szPage);
sqlite3Put4byte(&aWalHdr[12], pWal->nCkpt);
if( pWal->nCkpt==0 ) sqlite3_randomness(8, pWal->hdr.aSalt);
memcpy(&aWalHdr[16], pWal->hdr.aSalt, 8);
walChecksumBytes(1, aWalHdr, WAL_HDRSIZE-2*4, 0, aCksum);
sqlite3Put4byte(&aWalHdr[24], aCksum[0]);
sqlite3Put4byte(&aWalHdr[28], aCksum[1]);

pWal->szPage = szPage;
pWal->hdr.bigEndCksum = SQLITE_BIGENDIAN;
pWal->hdr.aFrameCksum[0] = aCksum[0];
pWal->hdr.aFrameCksum[1] = aCksum[1];
pWal->truncateOnCommit = 1;

rc = sqlite3OsWrite(pWal->pWalFd, aWalHdr, sizeof(aWalHdr), 0);
WALTRACE(("WAL%p: wal-header write %s\n", pWal, rc ? "failed" : "ok"));
if( rc!=SQLITE_OK ){
return rc;
}

/* Sync the header (unless SQLITE_IOCAP_SEQUENTIAL is true or unless
** all syncing is turned off by PRAGMA synchronous=OFF). Otherwise
** an out-of-order write following a WAL restart could result in
** database corruption. See the ticket:
**
** https://sqlite.org/src/info/ff5be73dee
*/
if( pWal->syncHeader ){
rc = sqlite3OsSync(pWal->pWalFd, CKPT_SYNC_FLAGS(sync_flags));
if( rc ) return rc;
}
}
if( (int)pWal->szPage!=szPage ){
return SQLITE_CORRUPT_BKPT; /* TH3 test case: cov1/corrupt155.test */
}

/* Setup information needed to write frames into the WAL */
w.pWal = pWal;
w.pFd = pWal->pWalFd;
w.iSyncPoint = 0;
w.syncFlags = sync_flags;
w.szPage = szPage;
iOffset = walFrameOffset(iFrame+1, szPage);
szFrame = szPage + WAL_FRAME_HDRSIZE;

/* Write all frames into the log file exactly once */
for(p=pList; p; p=p->pDirty){
int nDbSize; /* 0 normally. Positive == commit flag */

/* Check if this page has already been written into the wal file by
** the current transaction. If so, overwrite the existing frame and
** set Wal.writeLock to WAL_WRITELOCK_RECKSUM - indicating that
** checksums must be recomputed when the transaction is committed. */
if( iFirst && (p->pDirty || isCommit==0) ){
u32 iWrite = 0;
VVA_ONLY(rc =) walFindFrame(pWal, p->pgno, &iWrite);
assert( rc==SQLITE_OK || iWrite==0 );
if( iWrite>=iFirst ){
i64 iOff = walFrameOffset(iWrite, szPage) + WAL_FRAME_HDRSIZE;
void *pData;
if( pWal->iReCksum==0 || iWriteiReCksum ){
pWal->iReCksum = iWrite;
}
pData = p->pData;
rc = sqlite3OsWrite(pWal->pWalFd, pData, szPage, iOff);
if( rc ) return rc;
p->flags &= ~PGHDR_WAL_APPEND;
continue;
}
}

iFrame++;
assert( iOffset==walFrameOffset(iFrame, szPage) );
nDbSize = (isCommit && p->pDirty==0) ? nTruncate : 0;
rc = walWriteOneFrame(&w, p, nDbSize, iOffset);
if( rc ) return rc;
pLast = p;
iOffset += szFrame;
p->flags |= PGHDR_WAL_APPEND;
}

/* Recalculate checksums within the wal file if required. */
if( isCommit && pWal->iReCksum ){
rc = walRewriteChecksums(pWal, iFrame);
if( rc ) return rc;
}

/* If this is the end of a transaction, then we might need to pad
** the transaction and/or sync the WAL file.
**
** Padding and syncing only occur if this set of frames complete a
** transaction and if PRAGMA synchronous=FULL. If synchronous==NORMAL
** or synchronous==OFF, then no padding or syncing are needed.
**
** If SQLITE_IOCAP_POWERSAFE_OVERWRITE is defined, then padding is not
** needed and only the sync is done. If padding is needed, then the
** final frame is repeated (with its commit mark) until the next sector
** boundary is crossed. Only the part of the WAL prior to the last
** sector boundary is synced; the part of the last frame that extends
** past the sector boundary is written after the sync.
*/
if( isCommit && WAL_SYNC_FLAGS(sync_flags)!=0 ){
int bSync = 1;
if( pWal->padToSectorBoundary ){
int sectorSize = sqlite3SectorSize(pWal->pWalFd);
w.iSyncPoint = ((iOffset+sectorSize-1)/sectorSize)*sectorSize;
bSync = (w.iSyncPoint==iOffset);
testcase( bSync );
while( iOffsettruncateOnCommit && pWal->mxWalSize>=0 ){
i64 sz = pWal->mxWalSize;
if( walFrameOffset(iFrame+nExtra+1, szPage)>pWal->mxWalSize ){
sz = walFrameOffset(iFrame+nExtra+1, szPage);
}
walLimitSize(pWal, sz);
pWal->truncateOnCommit = 0;
}

/* Append data to the wal-index. It is not necessary to lock the
** wal-index to do this as the SQLITE_SHM_WRITE lock held on the wal-index
** guarantees that there are no other writers, and no data that may
** be in use by existing readers is being overwritten.
*/
iFrame = pWal->hdr.mxFrame;
for(p=pList; p && rc==SQLITE_OK; p=p->pDirty){
if( (p->flags & PGHDR_WAL_APPEND)==0 ) continue;
iFrame++;
rc = walIndexAppend(pWal, iFrame, p->pgno);
}
assert( pLast!=0 || nExtra==0 );
while( rc==SQLITE_OK && nExtra>0 ){
iFrame++;
nExtra--;
rc = walIndexAppend(pWal, iFrame, pLast->pgno);
}

if( rc==SQLITE_OK ){
/* Update the private copy of the header. */
pWal->hdr.szPage = (u16)((szPage&0xff00) | (szPage>>16));
testcase( szPage=65536 );
pWal->hdr.mxFrame = iFrame;
if( isCommit ){
pWal->hdr.iChange++;
pWal->hdr.nPage = nTruncate;
}
/* If this is a commit, update the wal-index header too. */
if( isCommit ){
walIndexWriteHdr(pWal);
pWal->iCallback = iFrame;
}
}

WALTRACE(("WAL%p: frame write %s\n", pWal, rc ? "failed" : "ok"));
return rc;
}

static int walRestartLog(Wal *pWal){
int rc = SQLITE_OK;
int cnt;

if( pWal->readLock==0 ){
volatile WalCkptInfo *pInfo = walCkptInfo(pWal);
assert( pInfo->nBackfill==pWal->hdr.mxFrame );
if( pInfo->nBackfill>0 ){
u32 salt1;
sqlite3_randomness(4, &salt1);
rc = walLockExclusive(pWal, WAL_READ_LOCK(1), WAL_NREADER-1);
if( rc==SQLITE_OK ){
/* If all readers are using WAL_READ_LOCK(0) (in other words if no
** readers are currently using the WAL), then the transactions
** frames will overwrite the start of the existing log. Update the
** wal-index header to reflect this.
**
** In theory it would be Ok to update the cache of the header only
** at this point. But updating the actual wal-index header is also
** safe and means there is no special case for sqlite3WalUndo()
** to handle if this transaction is rolled back. */
walRestartHdr(pWal, salt1);
walUnlockExclusive(pWal, WAL_READ_LOCK(1), WAL_NREADER-1);
}else if( rc!=SQLITE_BUSY ){
return rc;
}
}
walUnlockShared(pWal, WAL_READ_LOCK(0));
pWal->readLock = -1;
cnt = 0;
do{
int notUsed;
rc = walTryBeginRead(pWal, &notUsed, 1, &cnt);
}while( rc==WAL_RETRY );
assert( (rc&0xff)!=SQLITE_BUSY ); /* BUSY not possible when useWal==1 */
testcase( (rc&0xff)==SQLITE_IOERR );
testcase( rc==SQLITE_PROTOCOL );
testcase( rc==SQLITE_OK );
}
return rc;
}

static void walRestartHdr(Wal *pWal, u32 salt1){
volatile WalCkptInfo *pInfo = walCkptInfo(pWal);
int i; /* Loop counter */
u32 *aSalt = pWal->hdr.aSalt; /* Big-endian salt values */
pWal->nCkpt++;
pWal->hdr.mxFrame = 0;
sqlite3Put4byte((u8*)&aSalt[0], 1 + sqlite3Get4byte((u8*)&aSalt[0]));
memcpy(&pWal->hdr.aSalt[1], &salt1, 4);
walIndexWriteHdr(pWal);
AtomicStore(&pInfo->nBackfill, 0);
pInfo->nBackfillAttempted = 0;
pInfo->aReadMark[1] = 0;
for(i=2; iaReadMark = READMARK_NOT_USED;
assert( pInfo->aReadMark[0]==0 );
}

We highlighted the relevant pieces of the code above, now let's see how that translates into TLA+. To model the behavior we need, we focus on two actions in the code above: WalAppendTakeLock and WalAppend. We also need a new variable to represent the write lock (the first assert in the code above):

\* Lock needed to write to the WAL.
VARIABLE writeLock

WalAppendTakeLock ≜
∧ writeLock = "notTaken"
∧ writeLock' = "takenForAppend"
∧ UNCHANGED ⟨ wal, db, nBackfill, mxFrame, frameNumber, checkPointState, safeMxFrame, walSalt, pWalSalt ⟩

WalAppend ≜
∧ writeLock = "takenForAppend"
\* The if condition is written as an assert in the sqlite code because
\* checking for pWal->readLock == 0 gives us the same guarantee. If the
\* writer has taken the read lock at 0 it means there are no frames in the
\* wal that were not checkpointed.
∧ IF (nBackfill > 0 ∧ mxFrame = nBackfill)
THEN
\* Restart the Wal and Append.
\* We don't have readers so every writer after a checkpoint will
\* restart the wal.
∧ wal' = ⟨ frameNumber ⟩
∧ mxFrame' = 1
∧ nBackfill' = 0
∧ walSalt' = walSalt + 1
ELSE
∧ wal' = Append(wal, frameNumber)
∧ mxFrame' = mxFrame + 1
∧ UNCHANGED ⟨ nBackfill, walSalt ⟩
∧ frameNumber' = frameNumber + 1
∧ writeLock' = "notTaken"
∧ UNCHANGED ⟨ db, checkpoint_vars ⟩

Next, let's focus on checkpointing, which is the other piece of the puzzle:

SQLite code responsible for checkpointing
static int walCheckpoint(
Wal *pWal, /* Wal connection */
sqlite3 *db, /* Check for interrupts on this handle */
int eMode, /* One of PASSIVE, FULL or RESTART */
int (*xBusy)(void*), /* Function to call when busy */
void *pBusyArg, /* Context argument for xBusyHandler */
int sync_flags, /* Flags for OsSync() (or 0) */
u8 *zBuf /* Temporary buffer to use */
){
int rc = SQLITE_OK; /* Return code */
int szPage; /* Database page-size */
WalIterator *pIter = 0; /* Wal iterator context */
u32 iDbpage = 0; /* Next database page to write */
u32 iFrame = 0; /* Wal frame containing data for iDbpage */
u32 mxSafeFrame; /* Max frame that can be backfilled */
u32 mxPage; /* Max database page to write */
int i; /* Loop counter */
volatile WalCkptInfo *pInfo; /* The checkpoint status information */

szPage = walPagesize(pWal);
testcase( szPage=65536 );
pInfo = walCkptInfo(pWal);
if( pInfo->nBackfillhdr.mxFrame ){

/* EVIDENCE-OF: R-62920-47450 The busy-handler callback is never invoked
** in the SQLITE_CHECKPOINT_PASSIVE mode. */
assert( eMode!=SQLITE_CHECKPOINT_PASSIVE || xBusy==0 );

/* Compute in mxSafeFrame the index of the last frame of the WAL that is
** safe to write into the database. Frames beyond mxSafeFrame might
** overwrite database pages that are in use by active readers and thus
** cannot be backfilled from the WAL.
*/
mxSafeFrame = pWal->hdr.mxFrame;
mxPage = pWal->hdr.nPage;
for(i=1; iaReadMark+i); SEH_INJECT_FAULT;
if( mxSafeFrame>y ){
assert( yhdr.mxFrame );
rc = walBusyLock(pWal, xBusy, pBusyArg, WAL_READ_LOCK(i), 1);
if( rc==SQLITE_OK ){
u32 iMark = (i==1 ? mxSafeFrame : READMARK_NOT_USED);
AtomicStore(pInfo->aReadMark+i, iMark); SEH_INJECT_FAULT;
walUnlockExclusive(pWal, WAL_READ_LOCK(i), 1);
}else if( rc==SQLITE_BUSY ){
mxSafeFrame = y;
xBusy = 0;
}else{
goto walcheckpoint_out;
}
}
}

/* Allocate the iterator */
if( pInfo->nBackfillnBackfill, &pIter);
assert( rc==SQLITE_OK || pIter==0 );
}

if( pIter
&& (rc = walBusyLock(pWal,xBusy,pBusyArg,WAL_READ_LOCK(0),1))==SQLITE_OK
){
u32 nBackfill = pInfo->nBackfill;
pInfo->nBackfillAttempted = mxSafeFrame; SEH_INJECT_FAULT;

/* Sync the WAL to disk */
rc = sqlite3OsSync(pWal->pWalFd, CKPT_SYNC_FLAGS(sync_flags));

/* If the database may grow as a result of this checkpoint, hint
** about the eventual size of the db file to the VFS layer.
*/
if( rc==SQLITE_OK ){
i64 nReq = ((i64)mxPage * szPage);
i64 nSize; /* Current size of database file */
sqlite3OsFileControl(pWal->pDbFd, SQLITE_FCNTL_CKPT_START, 0);
rc = sqlite3OsFileSize(pWal->pDbFd, &nSize);
if( rc==SQLITE_OK && nSizehdr.mxFrame*szPage)pDbFd, SQLITE_FCNTL_SIZE_HINT,&nReq);
}
}

}

/* Iterate through the contents of the WAL, copying data to the db file */
while( rc==SQLITE_OK && 0==walIteratorNext(pIter, &iDbpage, &iFrame) ){
i64 iOffset;
assert( walFramePgno(pWal, iFrame)==iDbpage );
SEH_INJECT_FAULT;
if( AtomicLoad(&db->u1.isInterrupted) ){
rc = db->mallocFailed ? SQLITE_NOMEM_BKPT : SQLITE_INTERRUPT;
break;
}
if( iFramemxSafeFrame || iDbpage>mxPage ){
continue;
}
iOffset = walFrameOffset(iFrame, szPage) + WAL_FRAME_HDRSIZE;
/* testcase( IS_BIG_INT(iOffset) ); // requires a 4GiB WAL file */
rc = sqlite3OsRead(pWal->pWalFd, zBuf, szPage, iOffset);
if( rc!=SQLITE_OK ) break;
iOffset = (iDbpage-1)*(i64)szPage;
testcase( IS_BIG_INT(iOffset) );
rc = sqlite3OsWrite(pWal->pDbFd, zBuf, szPage, iOffset);
if( rc!=SQLITE_OK ) break;
}
sqlite3OsFileControl(pWal->pDbFd, SQLITE_FCNTL_CKPT_DONE, 0);

/* If work was actually accomplished... */
if( rc==SQLITE_OK ){
if( mxSafeFrame==walIndexHdr(pWal)->mxFrame ){
i64 szDb = pWal->hdr.nPage*(i64)szPage;
testcase( IS_BIG_INT(szDb) );
rc = sqlite3OsTruncate(pWal->pDbFd, szDb);
if( rc==SQLITE_OK ){
rc = sqlite3OsSync(pWal->pDbFd, CKPT_SYNC_FLAGS(sync_flags));
}
}
if( rc==SQLITE_OK ){
AtomicStore(&pInfo->nBackfill, mxSafeFrame); SEH_INJECT_FAULT;
}
}

/* Release the reader lock held while backfilling */
walUnlockExclusive(pWal, WAL_READ_LOCK(0), 1);
}

if( rc==SQLITE_BUSY ){
/* Reset the return code so as not to report a checkpoint failure
** just because there are active readers. */
rc = SQLITE_OK;
}
}

/* If this is an SQLITE_CHECKPOINT_RESTART or TRUNCATE operation, and the
** entire wal file has been copied into the database file, then block
** until all readers have finished using the wal file. This ensures that
** the next process to write to the database restarts the wal file.
*/
if( rc==SQLITE_OK && eMode!=SQLITE_CHECKPOINT_PASSIVE ){
assert( pWal->writeLock );
SEH_INJECT_FAULT;
if( pInfo->nBackfillhdr.mxFrame ){
rc = SQLITE_BUSY;
}else if( eMode>=SQLITE_CHECKPOINT_RESTART ){
u32 salt1;
sqlite3_randomness(4, &salt1);
assert( pInfo->nBackfill==pWal->hdr.mxFrame );
rc = walBusyLock(pWal, xBusy, pBusyArg, WAL_READ_LOCK(1), WAL_NREADER-1);
if( rc==SQLITE_OK ){
if( eMode==SQLITE_CHECKPOINT_TRUNCATE ){
/* IMPLEMENTATION-OF: R-44699-57140 This mode works the same way as
** SQLITE_CHECKPOINT_RESTART with the addition that it also
** truncates the log file to zero bytes just prior to a
** successful return.
**
** In theory, it might be safe to do this without updating the
** wal-index header in shared memory, as all subsequent reader or
** writer clients should see that the entire log file has been
** checkpointed and behave accordingly. This seems unsafe though,
** as it would leave the system in a state where the contents of
** the wal-index header do not match the contents of the
** file-system. To avoid this, update the wal-index header to
** indicate that the log file contains zero valid frames. */
walRestartHdr(pWal, salt1);
rc = sqlite3OsTruncate(pWal->pWalFd, 0);
}
walUnlockExclusive(pWal, WAL_READ_LOCK(1), WAL_NREADER-1);
}
}
}

walcheckpoint_out:
SEH_FREE_ON_ERROR(pIter, 0);
walIteratorFree(pIter);
return rc;
}

In TLA+ we need to split the function above into several different actions to model reading from shared memory, which can change in between reads! In fact, pInfo is a volatile pointer to the shared memory which can change, even without taking locks, for example by a concurrent writer. On the other hand, pWal is a copy of the wal-index header which does not change after the start of the execution.

\* checkpoint variables:
\* It is set using a copy of the wal-index header (pWal->hdr.mxFrame) when
\* starting the checkpoint.
VARIABLE safeMxFrame
\* It is set using a copy of the wal-index header (pWal->aSalt) when
\* starting the checkpoint.
VARIABLE pWalSalt
\* Running a checkpoint will move the state:
\* notStarted -> copiedHeader -> waitingForLock -> (finished) -> notStarted
\* Note that only one checkpoint can happen at a time, which is why this is a
\* global variable and that appends can happen concurrently with checkpoints,
\* the exclusion zones correspond to our atomic actions.
VARIABLE checkPointState

CheckPointCopyHeader ≜
∧ checkPointState = "notStarted"
∧ safeMxFrame' = mxFrame
∧ pWalSalt' = walSalt
∧ checkPointState' = "copiedHeader"
∧ UNCHANGED ⟨ wal, nBackfill, db, mxFrame, frameNumber, walSalt, writeLock ⟩

StartCheckpoint ≜
∧ checkPointState = "copiedHeader"
\* Important: here backfill is read from the live header while safeMxFrame
\* is read from the stale copy of the header.
∧ IF nBackfill < safeMxFrame
THEN checkPointState' = "waitingForLock"
ELSE checkPointState' = "notStarted"
∧ UNCHANGED ⟨ wal, nBackfill, db, mxFrame, frameNumber, safeMxFrame, walSalt, pWalSalt, writeLock ⟩

Checkpoint ≜
∧ checkPointState = "waitingForLock"
\* Move pages from wal into db.
∧ db' = db ∪ { wal[j] : j ∈ nBackfill+1‥Len(wal) }
∧ nBackfill' = safeMxFrame
\* Reset the checkpoint state.
∧ safeMxFrame' = 0
∧ pWalSalt' = 0
∧ checkPointState' = "notStarted"
∧ UNCHANGED ⟨ mxFrame, wal, frameNumber, walSalt, writeLock ⟩

You can download the full TLA+ specifications with instructions here: https://gist.github.com/letFunny/f068b46109d4b59f540df086429da05d .

4. Reproducing the bug

Once the model is in place, we can define an invariant that will trigger in the event of data loss or database corruption:

\* There are no "holes" in the database.
\* All the frames that were added to the WAL have landed in order.
NoPageIsLost ≜ ∀ f ∈ 1‥Cardinality(db) : f ∈ db

Running the model-checker quickly finds a counter-example. It takes only 20 states to witness a missing page in the database which can, as stated in the documentation, lead to database corruption. The sequence of states looks very similar to what is included in SQLite's own report of the bug, validating our model. Let's break it down, following the description of the bug from the SQLite docs :

writeLock
notTaken

checkPointState
notStarted

mxFrame
0

safeMxFrame
0

pWalSalt
0

nBackfill
0

walSalt
0

pageNumber
1

wal
[]

db
{}

writeLock
takenForAppend

checkPointState
notStarted

mxFrame
0

safeMxFrame
0

pWalSalt
0

nBackfill
0

walSalt
0

pageNumber
1

wal
[]

db
{}

writeLock
notTaken

checkPointState
notStarted

mxFrame
1

safeMxFrame
0

pWalSalt
0

nBackfill
0

walSalt
0

pageNumber
2

wal
[1]

db
{}

writeLock
takenForAppend

checkPointState
notStarted

mxFrame
1

safeMxFrame
0

pWalSalt
0

nBackfill
0

walSalt
0

pageNumber
2

wal
[1]

db
{}

writeLock
notTaken

checkPointState
notStarted

mxFrame
2

safeMxFrame
0

pWalSalt
0

nBackfill
0

walSalt
0

pageNumber
3

wal
[1, 2]

db
{}

writeLock
takenForAppend

checkPointState
notStarted

mxFrame
2

safeMxFrame
0

pWalSalt
0

nBackfill
0

walSalt
0

pageNumber
3

wal
[1, 2]

db
{}

writeLock
takenForAppend

checkPointState
copiedHeader

mxFrame
2

safeMxFrame
2

pWalSalt
0

nBackfill
0

walSalt
0

pageNumber
3

wal
[1, 2]

db
{}

writeLock
takenForAppend

checkPointState
waitingForLock

mxFrame
2

safeMxFrame
2

pWalSalt
0

nBackfill
0

walSalt
0

pageNumber
3

wal
[1, 2]

db
{}

writeLock
takenForAppend

checkPointState
notStarted

mxFrame
2

safeMxFrame
0

pWalSalt
0

nBackfill
2

walSalt
0

pageNumber
3

wal
[1, 2]

db
{1, 2}

writeLock
takenForAppend

checkPointState
copiedHeader

mxFrame
2

safeMxFrame
2

pWalSalt
0

nBackfill
2

walSalt
0

pageNumber
3

wal
[1, 2]

db
{1, 2}

writeLock
notTaken

checkPointState
copiedHeader

mxFrame
1

safeMxFrame
2

pWalSalt
0

nBackfill
0

walSalt
1

pageNumber
4

wal
[3]

db
{1, 2}

writeLock
takenForAppend

checkPointState
copiedHeader

mxFrame
1

safeMxFrame
2

pWalSalt
0

nBackfill
0

walSalt
1

pageNumber
4

wal
[3]

db
{1, 2}

writeLock
takenForAppend

checkPointState
waitingForLock

mxFrame
1

safeMxFrame
2

pWalSalt
0

nBackfill
0

walSalt
1

pageNumber
4

wal
[3]

db
{1, 2}

writeLock
takenForAppend

checkPointState
notStarted

mxFrame
1

safeMxFrame
0

pWalSalt
0

nBackfill
2

walSalt
1

pageNumber
4

wal
[3]

db
{1, 2, 3}

writeLock
takenForAppend

checkPointState
copiedHeader

mxFrame
1

safeMxFrame
1

pWalSalt
1

nBackfill
2

walSalt
1

pageNumber
4

wal
[3]

db
{1, 2, 3}

writeLock
notTaken

checkPointState
copiedHeader

mxFrame
2

safeMxFrame
1

pWalSalt
1

nBackfill
2

walSalt
1

pageNumber
5

wal
[3, 4]

db
{1, 2, 3}

writeLock
takenForAppend

checkPointState
copiedHeader

mxFrame
2

safeMxFrame
1

pWalSalt
1

nBackfill
2

walSalt
1

pageNumber
5

wal
[3, 4]

db
{1, 2, 3}

writeLock
notTaken

checkPointState
copiedHeader

mxFrame
1

safeMxFrame
1

pWalSalt
1

nBackfill
0

walSalt
2

pageNumber
6

wal
[5]

db
{1, 2, 3}

writeLock
notTaken

checkPointState
waitingForLock

mxFrame
1

safeMxFrame
1

pWalSalt
1

nBackfill
0

walSalt
2

pageNumber
6

wal
[5]

db
{1, 2, 3}

writeLock
notTaken

checkPointState
notStarted

mxFrame
1

safeMxFrame
0

pWalSalt
0

nBackfill
1

walSalt
2

pageNumber
6

wal
[5]

db
{1, 2, 3, 5}

[li]

Wal Append
Take Lock

[li]

Wal Append

Wal Append Take Lock

[li]

Wal Append

[li]

Wal Append
Take Lock

Checkpoint Copy Header

[li]

Start Checkpoint

[li]

Checkpoint

Checkpoint Copy Header

Wal Append

[li]

Wal Append
Take Lock

Start Checkpoint

[li]

Checkpoint

[li]

Checkpoint
Copy Header

Wal Append

[li]

Wal Append
Take Lock

[li]

Wal Append

Start Checkpoint

[li]

Checkpoint

[li]

STEP 2
[li]

STEP 3
[li]

STEP 4
[li]

STEP 5
[li]

STEP 6

⌃

⌄

writeLock
notTaken

checkPointState
notStarted

mxFrame
0

safeMxFrame
0

pWalSalt
0

nBackfill
0

walSalt
0

pageNumber
1

wal
[]

db
{}

writeLock
takenForAppend

checkPointState
notStarted

mxFrame
0

safeMxFrame
0

pWalSalt
0

nBackfill
0

walSalt
0

pageNumber
1

wal
[]

db
{}

writeLock
notTaken

checkPointState
notStarted

mxFrame
1

safeMxFrame
0

pWalSalt
0

nBackfill
0

walSalt
0

pageNumber
2

wal
[1]

db
{}

writeLock
takenForAppend

checkPointState
notStarted

mxFrame
1

safeMxFrame
0

pWalSalt
0

nBackfill
0

walSalt
0

pageNumber
2

wal
[1]

db
{}

writeLock
notTaken

checkPointState
notStarted

mxFrame
2

safeMxFrame
0

pWalSalt
0

nBackfill
0

walSalt
0

pageNumber
3

wal
[1, 2]

db
{}

writeLock
takenForAppend

checkPointState
notStarted

mxFrame
2

safeMxFrame
0

pWalSalt
0

nBackfill
0

walSalt
0

pageNumber
3

wal
[1, 2]

db
{}

writeLock
takenForAppend

checkPointState
copiedHeader

mxFrame
2

safeMxFrame
2

pWalSalt
0

nBackfill
0

walSalt
0

pageNumber
3

wal
[1, 2]

db
{}

writeLock
takenForAppend

checkPointState
waitingForLock

mxFrame
2

safeMxFrame
2

pWalSalt
0

nBackfill
0

walSalt
0

pageNumber
3

wal
[1, 2]

db
{}

writeLock
takenForAppend

checkPointState
notStarted

mxFrame
2

safeMxFrame
0

pWalSalt
0

nBackfill
2

walSalt
0

pageNumber
3

wal
[1, 2]

db
{1, 2}

[li]

Wal Append
Take Lock

[li]

Wal Append

Wal Append Take Lock

[li]

Wal Append

[li]

Wal Append
Take Lock

Checkpoint Copy Header

[li]

Start Checkpoint

[li]

Checkpoint

writeLock
takenForAppend

checkPointState
copiedHeader

mxFrame
2

safeMxFrame
2

pWalSalt
0

nBackfill
2

walSalt
0

pageNumber
3

wal
[1, 2]

db
{1, 2}

writeLock
notTaken

checkPointState
copiedHeader

mxFrame
1

safeMxFrame
2

pWalSalt
0

nBackfill
0

walSalt
1

pageNumber
4

wal
[3]

db
{1, 2}

writeLock
takenForAppend

checkPointState
copiedHeader

mxFrame
1

safeMxFrame
2

pWalSalt
0

nBackfill
0

walSalt
1

pageNumber
4

wal
[3]

db
{1, 2}

[li]

Wal Append
Take Lock

writeLock
takenForAppend

checkPointState
waitingForLock

mxFrame
1

safeMxFrame
2

pWalSalt
0

nBackfill
0

walSalt
1

pageNumber
4

wal
[3]

db
{1, 2}

writeLock
takenForAppend

checkPointState
notStarted

mxFrame
1

safeMxFrame
0

pWalSalt
0

nBackfill
2

walSalt
1

pageNumber
4

wal
[3]

db
{1, 2, 3}

writeLock
takenForAppend

checkPointState
copiedHeader

mxFrame
1

safeMxFrame
1

pWalSalt
1

nBackfill
2

walSalt
1

pageNumber
4

wal
[3]

db
{1, 2, 3}

[li]

Checkpoint

[li]

Checkpoint
Copy Header

writeLock
notTaken

checkPointState
copiedHeader

mxFrame
2

safeMxFrame
1

pWalSalt
1

nBackfill
2

walSalt
1

pageNumber
5

wal
[3, 4]

db
{1, 2, 3}

writeLock
takenForAppend

checkPointState
copiedHeader

mxFrame
2

safeMxFrame
1

pWalSalt
1

nBackfill
2

walSalt
1

pageNumber
5

wal
[3, 4]

db
{1, 2, 3}

writeLock
notTaken

checkPointState
copiedHeader

mxFrame
1

safeMxFrame
1

pWalSalt
1

nBackfill
0

walSalt
2

pageNumber
6

wal
[5]

db
{1, 2, 3}

[li]

Wal Append
Take Lock

[li]

Wal Append

writeLock
notTaken

checkPointState
waitingForLock

mxFrame
1

safeMxFrame
1

pWalSalt
1

nBackfill
0

walSalt
2

pageNumber
6

wal
[5]

db
{1, 2, 3}

writeLock
notTaken

checkPointState
notStarted

mxFrame
1

safeMxFrame
0

pWalSalt
0

nBackfill
1

walSalt
2

pageNumber
6

wal
[5]

db
{1, 2, 3, 5}

[li]

Checkpoint

Checkpoint Copy Header

Wal Append

Start Checkpoint

Wal Append

Start Checkpoint

STEP 1One connection does a checkpoint. This first checkpoint must be complete. In other words, the checkpoint must successfully copyall content from the WAL file back into the database and leave the WAL file in a state where it can potentially be reset.
STEP 2Shortly after the first checkpoint completes, a second checkpoint is started.
STEP 3While the second checkpoint from step 2 is starting up, another database connection commits a transaction that resets the WAL fileand writes new content into the beginning of the WAL file.
STEP 4Due to a data race, the second checkpoint from step 2 does not realize that the WAL file has been reset by the transaction commitin step 3. The second checkpoint leaves a field in the header of the WAL-Index set incorrectly. That field indicates that part ofthe WAL file has already been checkpointed, when in fact it has not been.
STEP 5Additional transactions are committed to increase the number of pages in the WAL file to be more than were present for the firstcheckpoint from step 1.
STEP 6Later when a third checkpoint occurs, the third checkpoint skips all or part of the transaction that was written in step 3. Thusparts of the transaction from step 3 never reach the database file, and the database file goes corrupt.

const STEPS = [{ "number": 1, "text": "One connection does a checkpoint. This first checkpoint must be complete. In other words, the checkpoint must successfully copy all content from the WAL file back into the database and leave the WAL file in a state where it can potentially be reset.", "targetY": 0 }, { "number": 2, "text": "Shortly after the first checkpoint completes, a second checkpoint is started.", "targetY": 626 }, { "number": 3, "text": "While the second checkpoint from step 2 is starting up, another database connection commits a transaction that resets the WAL file and writes new content into the beginning of the WAL file.", "targetY": 952 }, { "number": 4, "text": "Due to a data race, the second checkpoint from step 2 does not realize that the WAL file has been reset by the transaction commit in step 3. The second checkpoint leaves a field in the header of the WAL-Index set incorrectly. That field indicates that part of the WAL file has already been checkpointed, when in fact it has not been.", "targetY": 1278 }, { "number": 5, "text": "Additional transactions are committed to increase the number of pages in the WAL file to be more than were present for the first checkpoint from step 1.", "targetY": 1604 }, { "number": 6, "text": "Later when a third checkpoint occurs, the third checkpoint skips all or part of the transaction that was written in step 3. Thus parts of the transaction from step 3 never reach the database file, and the database file goes corrupt.", "targetY": 1930 }];
const VIEWBOX_HEIGHT = 2554;
const SCROLL_TOP = 12;
const SCROLL_H = 954;
const CAP_X = 16;
const CAP_W = 1148;
const CAP_Y = 970;
const svgDynamic = document.getElementById('tla-diagram');
const svgStatic = document.getElementById('tla-diagram-static');
const scrollContent = document.getElementById('scrollContent');
const captionStepEl = document.getElementById('caption-step');
const captionTextEl = document.getElementById('caption-text');
const prevEl = document.getElementById('previous');
const nextEl = document.getElementById('next');
let current = 0;
let animationFrame = null;
let currentScrollY = 0; // diagram-space Y at top of viewport

function setScrollY(y) {
currentScrollY = y;
scrollContent.setAttribute('transform', 'translate(70, ' + (SCROLL_TOP - y) + ')');
}

// Manual word-wrap for caption text using tspans
function wrapText(textEl, str, maxChars) {
while (textEl.firstChild) textEl.removeChild(textEl.firstChild);
const words = str.split(/\s+/);
const lines = [];
let line = '';
for (const w of words) {
const candidate = line ? line + ' ' + w : w;
if (candidate.length > maxChars && line) {
lines.push(line);
line = w;
} else {
line = candidate;
}
}
if (line) lines.push(line);
const x = textEl.getAttribute('x');
for (let i = 0; i < lines.length; i++) {
const ts = document.createElementNS('http://www.w3.org/2000/svg', 'tspan');
ts.setAttribute('x', x);
ts.setAttribute('dy', i === 0 ? '0' : '1.2em');
ts.textContent = lines;
textEl.appendChild(ts);
}
}

function renderCaption() {
captionStepEl.textContent = 'STEP ' + STEPS[current].number;
wrapText(captionTextEl, STEPS[current].text, 130);
}

function updateButtons() {
prevEl.setAttribute('opacity', current === 0 ? '0.28' : '1');
prevEl.setAttribute('pointer-events', current === 0 ? 'none' : 'auto');
nextEl.setAttribute('opacity', current === STEPS.length - 1 ? '0.28' : '1');
nextEl.setAttribute('pointer-events', current === STEPS.length - 1 ? 'none' : 'auto');
}

function animateScroll(target) {
if (animationFrame) cancelAnimationFrame(animationFrame);
const start = currentScrollY;
const distance = target - start;
const duration = 520;
const startTime = performance.now();
function tick(now) {
const progress = Math.min(1, (now - startTime) / duration);
const eased = 1 - Math.pow(1 - progress, 3);
setScrollY(start + distance * eased);
if (progress < 1) animationFrame = requestAnimationFrame(tick);
}
animationFrame = requestAnimationFrame(tick);
}

function goToStep(index) {
current = Math.max(0, Math.min(index, STEPS.length - 1));
renderCaption();
updateButtons();
animateScroll(STEPS[current].targetY);
}

prevEl.addEventListener('click', function () { goToStep(current - 1); });
nextEl.addEventListener('click', function () { goToStep(current + 1); });
document.addEventListener('keydown', function (event) {
if (event.key === 'ArrowUp' || event.key === 'ArrowLeft') goToStep(current - 1);
if (event.key === 'ArrowDown' || event.key === 'ArrowRight') goToStep(current + 1);
});

renderCaption();
updateButtons();
setScrollY(STEPS[0].targetY);
// Unhide the SVG now that everything is ready
svgDynamic.classList.remove('u-hide');
svgStatic.classList.add('u-hide');

And now, the all-important question...

5. Is dqlite affected?

To answer the question properly, we will create a model for dqlite that captures the differences with sqlite itself. We will then model-check again to see if the invariant breaks.

Given that dqlite needs to coordinate writes with Raft, it needs to be more restrictive with regards to which operations can proceed simultaneously. For this reason dqlite blocks any user-initiated checkpoint and disables automatic ones. Moreover, it will take more locks than SQLite usually needs to prevent both reads and writes from happening during a checkpoint – in practice, checkpoint is a stop-the-world action in dqlite. 

dqlite code that triggers a checkpoint from the VFS
static int vfsCheckpoint(sqlite3 *conn, struct vfsMainFile *f)
{
PRE(f->sharedMask == 0);
PRE(f->exclMask == 0);
tracef("[database %p] checkpoint start", (void*)f->database);

/* Try to lock everything, so that nothing can proceed. */
int rv = vfsShmLock(&f->database->shm, 0, SQLITE_SHM_NLOCK, true);
if (rv != SQLITE_OK) {
tracef("[database %p] checkpoint busy", (void*)f->database);
return rv;
}
f->exclMask = VFS__CHECKPOINT_MASK;

PRE(f->database->wal.n_tx == 0);

int wal_size;
int ckpt;
rv = sqlite3_wal_checkpoint_v2(conn, NULL, SQLITE_CHECKPOINT_TRUNCATE,
&wal_size, &ckpt);
/* Since no reader transaction is in progress, we must be able to
* checkpoint the entire WAL */
dqlite_assert(rv == SQLITE_OK);
dqlite_assert(wal_size == 0);
dqlite_assert(ckpt == 0);
tracef("[database %p] checkpointed", (void*)f->database);

f->exclMask = 0;
rv = vfsShmUnlock(&f->database->shm, 0, SQLITE_SHM_NLOCK, true);
dqlite_assert(rv == SQLITE_OK);

return SQLITE_OK;
}

As we can see above, the only difference for our model is that the write lock is taken before starting a checkpoint. TLA+ has a useful mechanism for extending existing specs by importing them with the INSTANCE keyword. We will use the base spec with the added locks on top:

SQLITE ≜ INSTANCE sqlite

DqliteCheckpointTakeLock ≜
∧ writeLock = "notTaken"
∧ writeLock' = "takenForCheckpoint"
∧ UNCHANGED ⟨ wal, db, nBackfill, mxFrame, frameNumber, checkPointState, safeMxFrame, walSalt, pWalSalt ⟩

DqliteCheckpointReleaseLock ≜
∧ writeLock = "takenForCheckpoint"
∧ checkPointState = "notStarted"
∧ writeLock' = "notTaken"
∧ UNCHANGED ⟨ wal, db, nBackfill, mxFrame, frameNumber, checkPointState, safeMxFrame, walSalt, pWalSalt ⟩

\* Overwrite the action in the original model by making sure the lock is taken.
DqliteCheckPointCopyHeader ≜
∧ writeLock = "takenForCheckpoint"
∧ SQLITE!CheckPointCopyHeader

\* Add two new actions for taking and releasing the lock.
DqliteNext ≜
∨ DqliteCheckpointTakeLock
∨ DqliteCheckpointReleaseLock
∨ SQLITE!Next

By reusing the same invariant we defined before, we can check if the changes to the spec will affect the bug. When model-checking we find that dqlite is not affected by the bug at all! This is because by taking the write lock for both appending and checkpointing, they cannot proceed simultaneously, and there is no data race.

6. Bonus: How was the bug fixed in SQLite?

On March 5, 2026 SQLite disclosed the bug and published a fix . A single extra check is enough to avoid the data race by checking that a reset of the WAL did not occur since we started the checkpoint:

SQLite code that fixes the bug

WalIndexHdr *pLive = (WalIndexHdr*)walIndexHdr(pWal);

/* Now that read-lock slot 0 is locked, check that the wal has not been
** wrapped since the header was read for this checkpoint. If it was, then
** there was no work to do anyway. In this case the
** (pInfo->nBackfillhdr.mxFrame) test above only passed because
** pInfo->nBackfill had already been set to 0 by the writer that wrapped
** the wal file. It would also be dangerous to proceed, as there may be
** fewer than pWal->hdr.mxFrame valid frames in the wal file. */
int bChg = memcmp(pLive->aSalt, pWal->hdr.aSalt, sizeof(pWal->hdr.aSalt));
if( 0==bChg ){
pInfo->nBackfillAttempted = mxSafeFrame; SEH_INJECT_FAULT

Checkpoint ≜
∧ checkPointState = waitingForLock"
∧ IF walSalt = pWalSalt
THEN
\* Move pages from wal into db.
∧ db' = db ∪ { wal[j] : j ∈ nBackfill+1‥Len(wal) }
∧ nBackfill' = safeMxFrame
ELSE
\* Salt changed, we skip the checkpoint.
∧ UNCHANGED ⟨ nBackfill, db ⟩
\* Reset the checkpoint state.
∧ safeMxFrame' = 0
∧ pWalSalt' = 0
∧ checkPointState' = notStarted"
∧ UNCHANGED ⟨ mxFrame, wal, pageNumber, walSalt, writeLock ⟩

Running the model-checker for the TLA+ model with the same invariant returns no error now, confirming the fix.

This article was written by Marco Manino and Alberto Carretero, dqlite team at Canonical. 1. Anatomy of a SQLite bug Recently SQLite published a new version with a fix to a long-standing bug in the way that the Write Ahead Log (WAL) is checkpointed that leads to the corruption of the database. The important aspect [...]


Categories: Dqlite
Source: https://ubuntu.com//blog/hunting-a-16-year-old-sqlite-bug-with-tla-is-dqlite-affected Jun 25, 2026, 12:03 PM

Ubuntu's 'Myna' project lets you talk instead of type – what is it?

Ubuntu is working on speech-to-text AI transcription so you can talk to type. It's powered by project Myna. Here's how it'll work and why it's adding it.

You're reading Ubuntu's 'Myna' project lets you talk instead of type – what is it? , a blog post from OMG! Ubuntu . Do not reproduce elsewhere without permission.


Categories: News, AI/ML, Explainer, Myna, Ubuntu 26.10
Source: https://www.omgubuntu.co.uk/2026/06/what-is-myna-ubuntu-ai-dictation Jun 30, 2026, 07:27 PM

This Flatpak runs a 30-year old version of GIMP – pre-GTK

Every wondered what famed FOSS image editor GIMP was like in 1996? Well, now you can find out. Developer balooii has packaged GIMP 0.54 into a Flatpak that runs on modern 64-bit Linux desktops with Wayland. It's apparently the earliest version of the app with the source code still available to build. This is not not an official GIMP effort, but a community effort. It's also something of a work-in-progress – of an ancient work-in-progress – with the maintainer promising they'll share more era-specific plugins and tutorials on using this ancient build in time. Before you skip to the install [...]

You're reading This Flatpak runs a 30-year old version of GIMP – pre-GTK , a blog post from OMG! Ubuntu . Do not reproduce elsewhere without permission.


Categories: News, GIMP, nostalgia
Source: https://www.omgubuntu.co.uk/2026/06/gimp-1996-flatpak Jun 29, 2026, 01:10 AM

Ubuntu 26.10 Snapshot 2 is out (with a 'breaking change')

Ubuntu 26.10 Snapshot 2 is available to download, the second of four snapshots planned for the 'Stonking Stingray' development cycle ahead of a stable release in October. As with the first snapshot, there's not a lot "new" stuff to see or test out, so unless you're a developer or an avid bug hunter there's little reason to rush off and try it. Canonical's Utkarsh Gupta, announcing the release on Ubuntu's developer mailing list, warns of a "breaking change" – don't panic: it's not in the image itself, but the URL it's accessed from. Over the past few weeks the Ubuntu [...]

You're reading Ubuntu 26.10 Snapshot 2 is out (with a 'breaking change') , a blog post from OMG! Ubuntu . Do not reproduce elsewhere without permission.


Categories: News, Monthly Snapshot, Ubuntu 26.10
Source: https://www.omgubuntu.co.uk/2026/06/ubuntu-26-10-snapshot-2-released Jun 26, 2026, 05:52 PM

Fed up with complex note taking apps? Try Whisp for Linux

Whisp is a Linux notes app with a difference. A gesture-driven GTK4/libadwaita UI offering a scratchpad for note taking. Inspired by Antinote for macOS.

You're reading Fed up with complex note taking apps? Try Whisp for Linux , a blog post from OMG! Ubuntu . Do not reproduce elsewhere without permission.


Categories: News, note taking apps, Whisp
Source: https://www.omgubuntu.co.uk/2026/06/whisp-linux-scratchpad Jun 26, 2026, 12:10 AM

Anbox Cloud on C4A metal: Android, at scale, without friction

Why C4A metal is a great place to run Android and why Anbox Cloud makes that practical.

If you've spent even a small portion of time working with Android development at scale, you've likely encountered some pinch points.

The platform was built for Arm-based devices, mobile physical hardware, and tightly controlled system environments. Cloud platforms, on the other hand, are optimized for abstraction, elasticity, and shared infrastructure. Anbox Cloud has already bridged this gap, enabling Android developers to scale virtual instances in the cloud efficiently. 

Yet, even with this flexibility, some use cases and workloads, like system-level Android development or large-scale Cuttlefish farms, call for native Arm performance and direct hardware access. For years, developers had to choose between genuine Android execution with physical device labs and cloud efficiency.

With the launch of Google Cloud's new Axion-based bare-metal instance, C4A metal, that trade-off starts to disappear. C4A-metal brings native Arm hardware directly into the cloud, without the performance limitations or complexity of nested virtualization. For Android workloads, this is a big deal.

And it's the perfect fit with Anbox Cloud.



Anbox Cloud is Canonical's platform for running Android at scale in cloud environments. It was built to manage, scale, and stream large numbers of Android instances reliably, whether for testing, CI/CD integration, automation, or interactive remote access.

On C4A metal, Anbox Cloud can run and orchestrate large fleets of Android systems directly on Arm hardware. There's nothing special to configure, no alternative workflows to learn. You provision C4A metal, deploy Anbox Cloud, and Android workloads run exactly as you would expect, only now with native performance and cloud elasticity.

"Anbox Cloud's support for fully virtualized Android provides an execution environment that closely matches the assumptions of AOSP and reference platforms such as Cuttlefish," says Alistair Delva from Google's Cloud Android team. "By allowing full Android system images, including the kernel, to run unmodified on scalable cloud and bare-metal infrastructure, such as C4A metal, Anbox Cloud enables system-level Android development, validation, and compliance workflows to move to the cloud with a level of fidelity that has traditionally required physical device labs. This combination of platform fidelity and cloud-scale operation represents a meaningful step forward for how Android systems can be built, tested, and operated." 

From a developer's point of view, this is where things get interesting. Android instances start quickly, can be scaled up and down programmatically and effortlessly, and can be accessed remotely through streaming when needed. From a platform point of view, everything is automated, observable, and reproducible.

It just works.

Scalable Cuttlefish environments, finally done right

One of the most compelling use cases for C4A metal is running large-scale Cuttlefish environments.

Android Cuttlefish is widely used for Android platform development and system validation, but it has traditionally been difficult to scale. Physical labs don't grow on demand, and running virtual devices on top of virtual machines quickly becomes inefficient and non-representative.

C4A metal removes that bottleneck. Anbox Cloud can launch and manage many Cuttlefish-based Android systems directly on bare metal, with no nested virtualization. The result is a cloud-native Cuttlefish farm that behaves like real hardware but scales like cloud infrastructure.

For Android platform teams, automotive OEMs, and system developers, this means faster feedback cycles, higher parallelism, and far less operational overhead.

Not just bare metal: one platform across C4A and N4A

Bare metal is powerful, but it's not the whole story.

Thanks to our close collaboration with Google Cloud, Anbox Cloud is designed to run across the Axion portfolio. Teams can use C4A metal for high-fidelity system testing while running build pipelines, orchestration services, and supporting infrastructure on C4A or N4A instances. The same Anbox Cloud deployment can span all of these environments without changing tools or workflows.

This flexibility is the real value. You don't need to choose between realism and efficiency up front. You can place each part of your Android workflow on the infrastructure that fits it best, and still operate everything as a single, coherent platform.

A natural fit for modern Android development

Android was built for Arm. C4A metal brings Arm-native bare metal into the cloud. Anbox Cloud connects the two with a platform that knows how to run, scale, and stream Android reliably.

Together, they make Android development simpler, faster, and more scalable, without asking teams to compromise on performance or fidelity.

As Android workloads continue to grow beyond apps into full systems and platforms, having infrastructure that matches Android's assumptions matters. With C4A metal and Anbox Cloud, that infrastructure is finally available as an on-demand cloud service.

Try Anbox Cloud on C4A metal now and stay tuned for further developments in our upcoming releases. For detailed instructions on how to upgrade your existing deployment, please refer to the Anbox Cloud documentation.

Further reading

Learn more about Anbox Cloud or contact our team to discuss your use case

Android is a trademark of Google LLC.

Anbox Cloud uses assets available through the Android Open Source Project.

The Android robot is reproduced or modified from work created and shared by Google and used according to terms described in theCreative Commons  3.0 Attribution License.

Why C4A metal is a great place to run Android and why Anbox Cloud makes that practical. If you've spent even a small portion of time working with Android development at scale, you've likely encountered some pinch points. The platform was built for Arm-based devices, mobile physical hardware, and tightly controlled system environments. Cloud platforms, [...]


Categories: Anbox, anbox cloud, Anbox Cloud Appliance
Source: https://ubuntu.com//blog/anbox-cloud-on-c4a-metal-android-at-scale-without-friction Jun 24, 2026, 02:31 PM

Canonical announces live kernel patching for Arm64

Canonical Livepatch  now officially supports Arm64, further expanding its security patching automation capabilities.

For the first time, Ubuntu on an Arm64 machine can apply critical kernel updates, without service interruption or rebooting. Starting with Ubuntu Core 26 for Arm64, and for Ubuntu Core 20 and onwards for AMD64 machines, a wider range of devices and cloud virtual machines can achieve timely vulnerability remediation through Canonical Livepatch. This enhancement will strengthen the security of systems that aren't security maintained daily or weekly, and provides an operational advantage for organizations working towards Cyber Resilience Act (CRA)  compliance.

Getting to this point was no small feat. In this article, we'll be looking back at the significant technical hurdles that stood in the way just a few years ago, so we can fully appreciate the meaning of this milestone. 

2023: the beginning

In late 2023, we conducted a comprehensive gap analysis to determine what it would take to bring live kernel patching to Arm64 processors. At the time, while Ubuntu provided Arm64 builds for nearly every released kernel, the ecosystem simply wasn't ready to support live kernel patching on this architecture.

Live kernel patching requires the kernel to know exactly when it is safe to switch a running task to patched code. This relies heavily on reliable kernel stack traces (CONFIG_HAVE_RELIABLE_STACKTRACE). The upstream Arm64 kernel lacked a stable, fully accepted implementation for reliable kernel stack traces at the time. Furthermore, the toolchain required to compile and compare unpatched and patched kernels, including GCC, objdump, and Kpatch, lacked mature Arm64 support. While pull requests and patches existed (some dating back to 2021), they were still under intense discussion and not fully merged upstream.

2024–2026: the work really starts

With the proliferation of high-performance Arm processors in cloud environments and increase in complex edge devices, solving this puzzle became an industry-wide imperative. Turning that 2023 gap analysis into today's reality required a monumental, coordinated effort between engineers at major OS publishers, hyperscalers, silicon vendors, and the broader open source community. Once the toolchain prerequisites, kernel consistency model for Arm64, and the implementation of reliable stack trace checks were finally merged upstream, the critical safety net required to swap code in a running kernel was officially in place. 

In anticipation of these upstream developments, our engineers ensured that Livepatch server and client were capable of distributing and managing arm64 live kernel patches. Once we had the tooling from upstream to produce loadable, cumulative kernel modules for Arm64 processors, we began testing, and putting our kernel build infrastructure through its paces.

Behind the scenes, our infrastructure teams went to work. Building live kernel patches requires compiling two copies of the Linux kernel because we test patches cumulatively for many kernels, on many Ubuntu versions, and on many architectures, the testing process represents an enormous computational requirement over time. Engineers orchestrate build farms to compile live kernel patches on target architectures, using the same compiler as the kernel. 

For performance and correctness, we do not use architecture emulation for building or testing live kernel patches. We expanded our build farms with dedicated Arm64 instances, boosting performance to handle the heavy computational load of native compilation across hundreds of rolling kernel patches. We also built entirely new, architecture-specific regression test suites to guarantee that an Arm64 livepatch would be as stable as our AMD64 patches. Finally, we overhauled our livepatch distribution network and clients, ensuring seamless, multi-architecture delivery. In late February the Arm64 Livepatch client for Ubuntu 26.04 LTS and Ubuntu Core 26 was applying live kernel patches in our test environments.

The present, and where we're going next

Today, the culmination of all this live kernel patching work for Arm64 is available in Ubuntu 26.04 LTS and Ubuntu Core 26. 

We have closed the technical gaps of recent years, replaced by a robust, scalable pipeline that delivers rebootless security patches directly to your Arm64 infrastructure. Whether you are managing a fleet of remote edge devices or scaling out Arm-based cloud servers, and your systems are not security patched and rebooted daily or weekly, then Canonical Livepatch serves as a key tool for maintaining a trusted and available fleet.

Related articles

• How is Livepatch safeguarded against bad actors?
• Mythbusting the scope of Livepatch protection
• Live Linux kernel patching with progressive timestamped rollouts

Canonical Livepatch now officially supports Arm64, further expanding its security patching automation capabilities. For the first time, Ubuntu on an Arm64 machine can apply critical kernel updates, without service interruption or rebooting. Starting with Ubuntu Core 26 for Arm64, and for Ubuntu Core 20 and onwards for AMD64 machines, a wider range of devices and [...]


Categories: livepatch
Source: https://ubuntu.com//blog/canonical-announces-live-kernel-patching-for-arm64 Jun 23, 2026, 03:01 AM