raid4.py

#!/usr/bin/env python2
from z3 import *
import math

# RAID-4 Non-Rotating Parity 0

class RealBlock(object):
    def __init__(self, k, i, j, v):
        self.k = k
        self.i = i
        self.j = j
        self.data = BitVec('block_{}'.format(v), 4096)
        print self.data

class RAIDArray(object):
    def __init__(self, L, M, N):
        '''
        L is strip depth
        M is no. of blocks in virtual disk
        N is no. of extents
        '''

        if M % (N-1) != 0:
            raise ValueError("M must be evenly divisible by N-1")

        if N < 3:
            raise ValueError("Minimum # disks required (N) for RAID-4 is 3")

        self.s = Solver()

        self.L, self.M, self.N = L, M, N
        # self.L, self.M, self.N = Ints('L M N')
        # L, M, N = self.l, self.m, self.n

        self.blocks = [RealBlock(x % L, ((x/L) % N-1) + 1, (x/L) / N-1, x) for x in range(M)]

        # print self.blocks

        self.parity_blocks = [RealBlock(k, 0, j, '{}_0_{}'.format(k, j)) for j in range(1+((M-1)/L)/N) for k in range(L)]

        # print self.parity_blocks
        # self.i, self.j, self.k, self.x = Ints('i j k x')
        #
        # self.s.add(self.i >= 0, self.i < N)
        # self.s.add(self.j >= 0, self.j <= (((M - 1) / L) / N - 1))
        # self.s.add(self.k >= 0, self.k < L)
        # self.s.add(self.x >= 0, self.x < M)

    def parity_block(self, k, p, j):
        pb = RealBlock(k, p, j)
        pb.block = reduce(BitVec.__xor__, [self.blocks[i].data for i in range(1, N)])
        return pb

# Define a virtual disk
# block# x = 0 to M-1 (M divisible by N-1)
#
# Define a array of disks participating in RAID
## N - No. of extents? 3 to 7
## Ordering of parity blocks (L to R or vice versa)
## Ordering of blocks (restart/continuing)
## L - Stripe depth (no. of blocks per strip), e.g. 4
## Size of block in bytes (2 bytes -> 4096 bytes)
## No. of stripes (function of number of blocks M)
#
# Mapping function from VD to RD
# virtual_block (x) = extent_block (MOD(x,L),
#                                   MOD(FLOOR(x/L), N-1) + 1,
#                                   FLOOR(FLOOR(x/L) / N-1))

# Index variables for each real block (k, i, j)
## k -- 0 to L-1 (depth/offset of block in the strip)
## i -- 0 to N-1 (extent index)
## j -- 0 to FLOOR(FLOOR((M-1)/L)/N-1) (stripe index)

# parity_block (k, 0, j) = reduce(BitVec.__xor__, [extent_block(k, i, j) for i in range(1, N))

if __name__ == "__main__":
    a = RAIDArray(4, 48, 5)
    # print(a.verify())