Characterizing Data Dependence Constraints for Dynamic Reliability Using n-Queens Attack Domains

Eric W. D. Rozier, Kristin Y. Rozier, Ulya Bayram


As data centers attempt to cope with the exponential growth of data, new techniques for intelligent, software-defined data centers (SDDC) are being developed to confront the scale and pace of changing resources and requirements.  For cost-constrained environments, like those increasingly present in scientific research labs, SDDCs also may provide better reliability and performability with no additional hardware through the use of dynamic syndrome allocation. To do so, the middleware layers of SDDCs must be able to calculate and account for complex dependence relationships to determine an optimal data layout.  This challenge is exacerbated by the growth of constraints on the dependence problem when available resources are both large (due to a higher number of syndromes that can be stored) and small (due to the lack of available space for syndrome allocation). We present a quantitative method for characterizing these challenges using an analysis of attack domains for high-dimension variants of the $n$-queens problem that enables performable solutions via the SMT solver Z3. We demonstrate correctness of our technique, and provide experimental evidence of its efficacy; our implementation is publicly available.


SMT; Data dependence; n-queens

Full Text:



Joseph A. Akinyele, Matthew Green, and Susan Hohenberger. Using SMT solvers to automate design tasks for encryption and signature schemes. In Ahmad-Reza Sadeghi, Virgil D. Gligor, and Moti Yung, editors, 2013 ACMSIGSAC Conference on Computer and Communications Security, CCS'13, Berlin, Germany, November 4-8, 2013, pages 399-410. ACM, 2013. URL:

H. Peter Anvin. The mathematics of RAID-6, 2007.

Ulya Bayram, Eric William Davis Rozier, Pin Zhou, and Dwight Divine. Improving reliability with dynamic syndrome allocation in intelligent software defined data centers. In 45th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2015, Rio de Janeiro, Brazil, June 22-25, 2015, pages 219-230. IEEE Computer Society, 2015. URL:

Ulya Bayram, Kristin Yvonne Rozier, and Eric William Davis Rozier. Characterizing data dependence constraints for dynamic reliability using N-queens attack domains. In Javier Campos and Boudewijn R. Haverkort, editors, Quantitative Evaluation of Systems, 12th International Conference, QEST 2015, Madrid, Spain, September 1-3, 2015, Proceedings, volume 9259 of Lecture Notes in Computer Science, pages 211-227. Springer, 2015. URL:

Jordan Bell and Brett Stevens. A survey of known results and research areas for n-queens. Discrete Mathematics, 309(1):1-31, 2009. URL:

Peter M. Chen, Edward K. Lee, Garth A. Gibson, Randy H. Katz, and David A. Patterson.RAID: high-performance, reliable secondary storage. ACM Computing Surveys (CSUR), 26(2):145-185, 1994. URL:

Peter F. Corbett, Robert English, Atul Goel, Tomislav Grcanac, Steven Kleiman, James Leong, and Sunitha Sankar. Row-diagonal parity for double disk failure correction. In Chandu Thekkath, editor, Proceedings of the FAST'04 Conference on File and Storage Technologies, March 31 - April 2, 2004, Grand Hyatt Hotel, San Francisco, California, USA, pages 1-14. USENIX, 2004. URL:

Leonardo Mendonça de Moura and Nikolaj Bjørner.Z3: an efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science, pages 337-340. Springer, 2008. URL:

Alexandros G. Dimakis, Brighten Godfrey, Martin J. Wainwright, and Kannan Ramchandran. Network coding for distributed storage systems. In INFOCOM 2007. 26th IEEE International Conference on Computer Communications, Joint Conference of the IEEE Computer and Communications Societies, 6-12 May 2007, Anchorage, Alaska, USA, pages 2000-2008. IEEE, 2007. URL:

Daniel Duffy and John Schnase. Meeting the big data challenges of climate science through cloud-enabled climate analytics-as-a-service. In Proceedings of the 30th International Conference on Massive Storage Systems and Technology. IEEE Computer Society, 2014.

B. Eickenscheidt. Das n-damen-problem auf dem zylinderbrett. feenschach, 50:382-385, 1980.

Ibrahim Abaker Targio Hashem, Ibrar Yaqoob, Nor Badrul Anuar, Salimah Mokhtar, Abdullah Gani, and Samee Ullah Khan. The rise of "big data" on cloud computing: Review and open research issues. Inf. Syst., 47:98-115, 2015. URL:

Casey Henderson. Usenix association fast 2013 memo, 2015. URL:

Nathan Jacobson. Lectures in Abstract Algebra: III. Theory of Fields and Galois Theory, volume 32. Springer Science & Business Media, 2012. URL:

M. C. Jones. Kumaraswamy?s distribution: A beta-type distribution with some tractability advantages. Statistical Methodology, 6(1):70-81, 2009. URL:

David A. Klarner. Queen squares. J. Recreational Math, 12(3):177-178, 1979.

Vladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark A. Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, and Benjamin Weiß. The 1st verified software competition: Experience report. In Michael J. Butler and Wolfram Schulte, editors, FM 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings, volume 6664 of Lecture Notes in Computer Science, pages 154-168. Springer, 2011. URL:

Ali Sinan Köksal, Viktor Kuncak, and Philippe Suter. Scala to the power of Z3: integrating SMT and programming. In Nikolaj Bjørner and Viorica Sofronie-Stokkermans, editors, Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings, volume 6803 of Lecture Notes in Computer Science, pages 400-406. Springer, 2011. URL:

Ponnambalam Kumaraswamy. A generalized probability density function for double-bounded random processes. Journal of Hydrology, 46(1):79-88, 1980. URL:

Adam Leventhal. Triple-parity RAID and beyond.ACM Queue, 7(11):30, 2009. URL:

Carl P. McCarty. Queen squares. The American Mathematical Monthly, 85(7):578-580, 1978. URL:

Bernard A. Nadel. Representation selection for constraint satisfaction: A case study using n-queens.IEEE Expert, 5(3):16-23, 1990. URL:

Jehan-François Pâris, Ahmed Amer, and Thomas J. E. Schwarz. Low-redundancy two-dimensional RAID arrays. In International Conference on Computing, Networking and Communications, ICNC 2012, Maui, HI, USA, January 30 - February 2, 2012, pages 507-511. IEEE Computer Society, 2012. URL:

Jehan-François Pâris, Darrell D. E. Long, and Witold Litwin. Three-dimensional redundancy codes for archival storage. In 2013 IEEE 21st International Symposium on Modelling, Analysis and Simulation of Computer and Telecommunication Systems, San Francisco, CA, USA, August 14-16, 2013, pages 328-332. IEEE Computer Society, 2013. URL:

David A. Patterson, Garth A. Gibson, and Randy H. Katz. A case for redundant arrays of inexpensive disks (RAID). In Haran Boral and Per-Åke Larson, editors, Proceedings of the 1988 ACMSIGMOD International Conference on Management of Data, Chicago, Illinois, June 1-3, 1988., pages 109-116. ACM Press, 1988. URL:

Vera Pless. Introduction to the Theory of Error-Correcting Codes, 3rd Edition. John Wiley & Sons, 1998.

Eric W. D. Rozier and Kristin Yvonne Rozier.SMT-driven intelligent storage for big data. In Proceedings of the Ninth International Workshop on Constraints in Formal Verification (CFV 2015), Austin, Texas, U.S.A., November 2015.

Eric W. D. Rozier and Kristin Yvonne Rozier. Cascading solution of data dependence constraints with Z3. In Proceedings of the Fourteenth International Symposium on Artificial Intelligence and Mathematics (ISAIM 2016), Fort Lauderdale, Florida, U.S.A., January 2016.

Eric William David Rozier and William H. Sanders. A framework for efficient evaluation of the fault tolerance of deduplicated storage systems. In Robert S. Swarz, Philip Koopman, and Michel Cukier, editors, IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2012, Boston, MA, USA, June 25-28, 2012, pages 1-12. IEEE Computer Society, 2012. URL:

Eric William David Rozier, William H. Sanders, Pin Zhou, NagaPramod Mandagere, Sandeep Uttamchandani, and Mark L. Yakushev. Modeling the fault tolerance consequences of deduplication. In 30th IEEE Symposium on Reliable Distributed Systems (SRDS 2011), Madrid, Spain, October 4-7, 2011, pages 75-84. IEEE Computer Society, 2011. URL:

Eric William David Rozier, Pin Zhou, and Dwight Divine. Building intelligence for software defined data centers: modeling usage patterns. In Ronen I. Kat, Mary Baker, and Sivan Toledo, editors, 6th Annual International Systems and Storage Conference, SYSTOR'13, Haifa, Israel - June 30 - July 02, 2013, page 20. ACM, 2013. URL:

Miguel A Salido and Federico Barber. How to classify hard and soft constraints in non-binary constraint satisfaction problems. In Research and Development in Intelligent Systems XX: Proceedings of AI2003, the Twenty-third SGAI International Conference on Innovative Techniques and Applications of Artificial Intelligence, pages 213-226. Springer London, London, 2004. URL:

John L. Schnase, Daniel Q. Duffy, Glenn S. Tamkin, Denis Nadeau, John H. Thompson, Cristina M. Grieg, Mark A. McInerney, and William P. Webster. Merra analytic services: Meeting the big data challenges of climate science through cloud-enabled climate analytics-as-a-service. Computers, Environment and Urban Systems, 61, Part B:98-211, 2017. URL:

Thomas J. E. Schwarz, Darrell D. E. Long, and Jehan-François Pâris. Reliability of disk arrays with double parity. In IEEE 19th Pacific Rim International Symposium on Dependable Computing, PRDC 2013, Vancouver, BC, Canada, December 2-4, 2013, pages 108-117. IEEE Computer Society, 2013. URL:

Rok Sosic and Jun Gu. Efficient local search with conflict minimization: A case study of the n-queens problem.IEEE Trans. Knowl. Data Eng., 6(5):661-668, 1994. URL:

Vernon Turner, John F Gantz, David Reinsel, and Stephen Minton. The digital universe of opportunities: Rich data and the increasing value of the internet of things. International Data Corporation, White Paper, IDC_1672, 2014.

Eric W. Weisstein. Rooks problem, 2002.



Copyright (c) 2017 Eric W. D. Rozier, Kristin Y. Rozier, and Ulya Bayram

Creative Commons License CC BY
This work is licensed under a Creative Commons Attribution 3.0 Germany License (CC BY 3.0 DE).

License URL:

Published by the European Design and Automation Association (EDAA) \ EMbedded Systems Special Interest Group (EMSIG) and Schloss Dagstuhl -- Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing.