/* * Formal model for disk synchronization. * * Copyright (C) 2012 Red Hat, Inc. * Author: Paolo Bonzini * * State space explodes real fast: * * SEC \ MAX 1 2 3 * 2 170K 5M 48M * 3 17M ?? ?? * * and so does the amount of memory required to run verification, * so I didn't allow customizing the number of sectors beyond 3. */ /* Number of writes tested (max 255, good luck ;). */ #define MAX 3 /* Number of sectors tested (max 3). */ #define SEC 2 #define EXTRA_ASSERT byte cache_src[SEC]; /* Value written to the source (on cache) */ byte disk_src[SEC]; /* Value written to the source (on medium) */ byte cache_dest[SEC]; /* Value written to the destination (on cache) */ byte disk_dest[SEC]; /* Value written to the destination (on medium) */ bit cache_dirty[SEC]; /* Value of the persistent dirty bitmap (on cache) */ bit disk_dirty[SEC]; /* Value of the persistent dirty bitmap (on medium) */ bit volatile_dirty[SEC]; /* Value of the volatile dirty bitmap */ byte count; /* Number of bits set in the volatile dirty bitmap */ bit sim_done; #ifdef EXTRA_ASSERT /* Only used for extra assertion checks, not part of the algorithm. * Does not make verification substantially slower. */ bit in_flight[SEC]; #endif /* This process repeatedly tests assertions and checks for the end * of the run. */ active proctype assertions() { byte sector; do :: true -> atomic { sector = (sector + 1) % SEC; /* The cache must not have older data than the disk. */ assert(disk_src[sector] <= cache_src[sector]); assert(disk_dest[sector] <= cache_dest[sector]); /* Data cannot come from the future. :) */ assert(cache_dest[sector] <= cache_src[sector]); /* The volatile bitmap can say anything, but the persistent * bitmap must be clear only if the destination disk can * be recovered. Flushing the destination before the source * is fine. */ assert(cache_dirty[sector] || disk_dest[sector] >= disk_src[sector]); /* The persistent bitmap conservatively approximates the volatile * bitmap. */ assert(cache_dirty[sector] >= volatile_dirty[sector]); /* The count must be accurate. */ assert(count == (volatile_dirty[0] #if SEC > 1 + volatile_dirty[1] #endif #if SEC > 2 + volatile_dirty[2] #endif )); #if 0 if :: volatile_dirty[0] || cache_dirty[0] || disk_dirty[0] || disk_src[0] > disk_dest[0] || disk_src[0] < MAX #if SEC > 1 || volatile_dirty[1] || cache_dirty[1] || disk_dirty[1] || disk_src[1] > disk_dest[1] || disk_src[1] < MAX #endif #if SEC > 2 || volatile_dirty[2] || cache_dirty[2] || disk_dirty[2] || disk_src[2] > disk_dest[2] || disk_src[2] < MAX #endif :: else -> sim_done = 1; fi; #endif } od; } /* The OS can flush data to disk at arbitrary times. But data can be assumed * to never be on the source platters until an explicit flush. */ active proctype os() { do :: disk_dest[0] != cache_dest[0] -> disk_dest[0] = cache_dest[0]; :: disk_dirty[0] != cache_dirty[0] -> disk_dirty[0] = cache_dirty[0]; #if SEC > 1 :: disk_dest[1] != cache_dest[1] -> disk_dest[1] = cache_dest[1]; :: disk_dirty[1] != cache_dirty[1] -> disk_dirty[1] = cache_dirty[1]; #endif #if SEC > 2 :: disk_dest[2] != cache_dest[2] -> disk_dest[2] = cache_dest[2]; :: disk_dirty[2] != cache_dirty[2] -> disk_dirty[2] = cache_dirty[2]; #endif od; } active proctype writes() { byte sector; loop: if :: cache_src[0] < MAX -> atomic { sector = 0; goto write; } #if SEC > 1 :: cache_src[1] < MAX -> atomic { sector = 1; goto write; } #endif #if SEC > 2 :: cache_src[2] < MAX -> atomic { sector = 2; goto write; } #endif :: true -> goto flush; fi; write: #ifdef EXTRA_ASSERT in_flight[sector] = 1; #endif /* First write the data. */ cache_src[sector]++; /* Then update the persistent dirty bitmap. It's cheaper than copying * the volatile bitmap to the persistent bitmap on every flush. * * Updates to the bitmap have to be done under a lock, otherwise * the mirroring process can copy volatile_dirty to cache_dirty * at the point marked XXX. That would set cache_dirty[sector] * back to 0 even though the write hasn't reached disk_dest yet. * * When implementing this with coroutines the lock will be implicit, * because context switches can only happen in precise places. */ atomic { cache_dirty[sector] = 1; /* XXX */ count = count + !volatile_dirty[sector]; volatile_dirty[sector] = 1; #ifdef EXTRA_ASSERT in_flight[sector] = 0; #endif } goto loop; flush: /* Flush the data and the bitmap, any order will do. */ do :: disk_src[0] != cache_src[0] -> disk_src[0] = cache_src[0]; :: disk_dirty[0] != cache_dirty[0] -> disk_dirty[0] = cache_dirty[0]; #if SEC > 1 :: disk_src[1] != cache_src[1] -> disk_src[1] = cache_src[1]; :: disk_dirty[1] != cache_dirty[1] -> disk_dirty[1] = cache_dirty[1]; #endif #if SEC > 2 :: disk_src[2] != cache_src[2] -> disk_src[2] = cache_src[2]; :: disk_dirty[2] != cache_dirty[2] -> disk_dirty[2] = cache_dirty[2]; #endif :: else -> break; od; goto loop; } active proctype mirror() { byte sector; loop: /* Pick a sector, block until one is available. */ if :: volatile_dirty[0] -> sector = 0; #if SEC > 1 :: volatile_dirty[1] -> sector = 1; #endif #if SEC > 2 :: volatile_dirty[2] -> sector = 2; #endif fi; /* Update the volatile dirty bitmap. */ atomic { count = count - volatile_dirty[sector]; volatile_dirty[sector] = 0; } /* Copy the data */ cache_dest[sector] = cache_src[sector]; /* Check whether the data should be flushed. */ if :: count == 0 -> /* Flush the destination to disk. Writes can happen in the * meanwhile, and they will set count > 0. */ do :: disk_dest[0] != cache_dest[0] -> disk_dest[0] = cache_dest[0]; #if SEC > 1 :: disk_dest[1] != cache_dest[1] -> disk_dest[1] = cache_dest[1]; #endif #if SEC > 2 :: disk_dest[2] != cache_dest[2] -> disk_dest[2] = cache_dest[2]; #endif :: else -> break; od; /* Reset the persistent dirty bitmap under a lock. */ atomic { cache_dirty[0] = volatile_dirty[0]; #if SEC > 1 cache_dirty[1] = volatile_dirty[1]; #endif #if SEC > 2 cache_dirty[2] = volatile_dirty[2]; #endif #ifdef EXTRA_ASSERT assert(cache_dest[0] == cache_src[0] || volatile_dirty[0] || in_flight[0]); #if SEC > 1 assert(cache_dest[1] == cache_src[1] || volatile_dirty[1] || in_flight[1]); #endif #if SEC > 2 assert(cache_dest[2] == cache_src[2] || volatile_dirty[2] || in_flight[2]); #endif #endif } /* No need to flush the dirty bitmap to disk here. */ :: else -> skip; fi; goto loop; }