Please enter banners and links.
LOTOS17مقدمه ای بر جبر پروسه ها18
VDM-SL22
شبکه های پتری23
خصوصیات رفتاری25
Reachability26
Boundedness26
Liveness26
Reversibility28
Coverability28
زیر مجموعه های شبکه های پتری29
State Machine (SM)30
Marked Graph (MG)30
Free-choice net (FC)31
Extended Free-choice net (EFC)31
Asymmetric choice net (AC)31
قضایا و فرضیات32
مقایسه و جمع بندی35
فصل سوم: بررسی معماری دیتا سنترها38
Microsoft Hyper-V39
بررسی اجزاء معماری Hyper-V42
APIC43
Child Partition43
Hypercall43
Hypervisor43
IC43
I/O stack44
Root Partition44
VID44
VMBus44
VMMS44
VMWP44
VSC45
VSP45
WinHv45
WMI45
نقاط ضعف46
Xen46
بررسی اجزاء معماری Xen48
Xen Hypervisor48
Domain 048
Domain U49
Xenstored50
ارتباطات مابین دامنه صفر و دامنه های U50
VMware ESXi50
بررسی اجزاء معماری VMware ESX52
VMkernel52
File Sys–52
CIM53
طراحی یک معماری برای دیتا سنتر54
مختصری درباره vSphere56
سرویس های زیر ساختی vSphere58
سرویس های کاربردی vSphere59
سرور VMware vCenter59
Client ها59
ESX59
vCenter Server59
VMFS59
SMP60
VCMS60
VI Client60
VMware VMotion60
Storage VMotion60
VMware HA61
DRS62
Consolidated Backup63
vSphere SDK63
Fault Tolerance64
سرویس های توزیع شده در vSphare64
معماری شبکه64
معماری محل ذخیره سازی داده ها66
معماری سرور مدیریت VirtualCenter69
User Access Control70
Core Service71
جمع بندی71
فصل چهارم: ارائه مدل فرمال برای دیتا سنتر و تحلیل آن72
تشریح دیتا سنتر نمونه73
ارائه مدلی از رفتار کلی دیتا سنتر77
ارزیابی و تحلیل مدل فرمال87
4.2.1.1. Liveness87
4.2.1.2. Safeness87
4.2.1.3. Reversibility89
بررسی لایه های پایینتر مدل فرمال90
بررسی نحوه کار سرویس HA91
شرح سرویس VMware HA91
ارائه مدل فرمال از نحوه کار سرویس HA95
تحلیل و ارزیابی مدل98
4.3.3.1. Liveness99
4.3.3.2. Safeness101
4.3.3.3. Reversibility102
بررسی نحوه کار سرویس Fault Tolerance106
تشریح ساختار سرویس Fault Tolerance106
ارائه مدل فرمال از نحوه کار سرویس Fault Tolerance110
تحلیل و ارزیابی مدل111
4.4.3.1. Liveness112
4.4.3.2. Safeness113
4.4.3.3. Reversibility113
بررسی نحوه کار سرویس VMotion114
تشریح ساختار سرویس VMotion114
ارائه مدل فرمال از نحوه کار سرویس VMotion118
تحلیل و ارزیابی مدل119
4.5.3.1. Liveness120
4.5.3.2. Safeness121
4.5.3.3. Reversibility122
بررسی ساختار داخلی ESX hypervisor124
تشریح ساختار ESX124
ارائه یک مدل فرمال از نحوه کار ESX125
بررسی و تحلیل مدل129
4.6.3.1. Liveness129
4.6.3.2. Safeness131
4.6.3.3. Reversibility132
تشریح ساختار سیستم ذخیره سازی در ESX133
تشریح ساختار سیستم ذخیره سازی133
ارائه یک مدل فرمال از نحوه کار سیستم ذخیره سازی در ESX138
بررسی و تحلیل مدل144
4.7.3.1. Liveness144
4.7.3.2. Safeness145
4.7.3.3. Reversibility146
معماری ساختار شبکه در ESX148
تشریح ساختار شبکه148
ارائه مدل فرمال برای ساختار شبکه در ESX155
بررسی و تحلیل مدل161
4.8.3.1. Reversibility161
4.8.3.2. Liveness 163
4.8.3.3. Safeness165
معماری سوئیچ مجازی در ساختار شبکه165
تحلیل ساختار سوئیچ مجازی165
ارائه یک مدل فرمال برای سوئیچ مجازی169
بررسی و تحلیل مدل172
4.9.3.1. Liveness172
4.9.3.2. Safeness173
4.9.3.3. Reversibility174
جمع بندی175
فصل پنجم: نتیجه گیری و پیشنهادات176
مراجع180
پیوست: مجموعه کامل مدل های پتری طراحی شده در پایان نامه186
چکیده به زبان انگلیسی195
فهرست جدول ها
عنوان و شمارهصفحه
جدول 2.1. خلاصه مقایسه ابزار توصیف فرمال36
جدول 3.1. سیستم های عامل قابل پشتیبانی توسط Hyper-V R2 41
جدول 3.2. سیستم های عامل قابل پشتیبانی توسط Xen نسخه 3.47
جدول 4.1. گزارهای فعال در وضعیت های M0 الی M15 از مدل پتری 4.30164
جدول 5.1. خلاصه نتایج به دست آمده از تحلیل رفتار زیر سیستم ها و سرویس های VMware ESX177
فهرست شکل ها
عنوانصفحه
شکل 1.1. نحوه قرارگیری لایه های نرم افزاری بر روی سرور4
شکل 1.2. شمای کلی دیتا سنتر با معماری مجازی5
شکل 2.1. مثال هایی از زبان های فرمال و تقسیم بندی آنها ]10[13
شکل 2.2. روال طراحی یک سیستم نمونه به کمک زبان های فرمال ]10[14
شکل 2.3. نقطه gate در جبر پروسه ها ]4[18
شکل 2.4. مدل تولید کننده- مصرف کننده به کمک LOTOS ]17[19
شکل 2.5. مثالی از مدل سازی یک پروتکل به کمک شبکه های پتری ]23[25
شکل 2.6. نمونه ای از شبکه پتری non-Live ]23[27
شکل 2.7. نشانه گزاری برای: a) مجموعه موقعیت های ورودی و خروجی برای t و b) مجموعه گزارهای ورودی و خروجی برای p ]23[30
شکل 2.8. مثال هایی از زیر مجموعه های شبکه های پتری ]23[32
شکل 2.9. یک شبکه پتری و گراف نشانه دار مربوط به آن ]23[33
شکل 3.1. معماری سطح بالای Hyper-V ]40[42
شکل 3.2. شمایی از معماری Xen ]51[47
شکل 3.3. نحوه سرویس دهی به ماشین میزبان توسط Qemu-DM ]51[49
شکل 3.4. شمایی از معماری VMware ESXi ]3[52
شکل 3.5. ساختار شماتیک مدیریت CIM ]3[54
شکل 3.6. مثالی از مفاهیم میزبان، کلاستر و مخزن منابع ]60[58
شکل 3.7. طرز کار سرویس HA ]61[62
شکل 3.8. شمایی از معماری شبکه در محیط مجازی ]60[65
شکل 3.9. شمایی از معماری ذخیره سازی ]60[66
شکل 3.10. طرز کار RDM ]60[68
شکل 3.11. شمایی از ساختار سرور مدیریت VirtualCenter ]60[70
شکل 4.1. زیر ساخت دیتا سنتر مجازی ]63[73
شکل 4.2. یک الگوی نمونه برای زیر ساخت دیتا فیزیکی سنتر ]60[75
شکل 4.3. ساختار شماتیک دیتا سنتر نمونه76
شکل 4.4. مدل پتری طراحی شده برای دیتا سنتر نمونه78
شکل 4.5. گراف پوشا برای مدل پتری شکل 4.488
شکل 4.6. نتیجه تحلیل فضای حالت به وسیله نرم افزار PIPE89
شکل 4.7. مدل پتری نحوه کار سرویس HA96
شکل 4.8. عضویت شبکه 4.7 در زیرکلاس های شبکه های پتری100
شکل 4.9. گراف پوشای مدل 4.7101
شکل 4.10. نتیجه تحلیل فضای حالت بر روی مدل102
شکل 4.11. نحوه توزیع توکن در وضعیت S8103
شکل 4.12. شبیه سازی شبکه پتری شکل 4.7104
شکل 4.13. چندین نمونه از شبیه سازی اجرای شبکه پتری105
شکل 4.14. مدل پتری نحوه کار سرویس Fault Tolerance110
شکل 4.15. نحوه توزیع توکن ها در M3 و M4112
شکل 4.16. گراف پوشای مدل پتری شکل 4.14114
شکل 4.17 مدل پتری نحوه کار سرویس VMotion118
شکل 4.18. گراف نشانه دار (G, ) مربوط به مدل 4.17120
شکل 4.19. گراف پوشای مدل 4.17123
شکل 4.20. مدل پتری طرز کار ESX125
شکل 4.21. گراف جهت دار معادل شبکه پتری 4.20130
شکل 4.22. گراف پوشای کدل پتری 4.20132
شکل 4.23. نمای شماتیک مدل چند لایه ای سیستم ذخیره سازی در ESX ]63[134
شکل 4.24. مدل پتری ارائه شده از نحوه کار سیستم ذخیره سازی در ESX139
شکل 4.25. گراف جهت دار متناظر با مدل پتری 4.24144
شکل 4.26. گراف پوشای شبکه پتری 4.24146
شکل 4.27. نرم افزار تحلیلگر گراف، در حال اجرای الگوریتم اول عمق147
شکل 4.28. نحوه ارتباط کارت شبکه مجازی و سوئیچ مجازی ]62[149
شکل 4.29. شمای کلی از ساختار شبکه در سرور ESX153
شکل 4.30. مدل پتری تهیه شده از ساختار شبکه در ESX156
شکل 4.31. گراف پوشای مدل پتری شکل 4.30162
شکل 4.32. جستجوی اول عمق گراف شکل 4.31163
شکل 4.33 مدل فرمال از نحوه کار سوئیچ مجازی170
شکل 4.34. گراف جهت دار متناظر با مدل پتری 4.33173
شکل 4.35. گراف پوشای مدل پتری 4.33174
فصل اول: مقدمه
بیان مسئله و ضرورت تحقیقنیاز بشر به پردازش و ذخیره سازی اطلاعات در دهه های گذشته همواره رشد صعودی و شتابدار داشته است. به گونه ای که حرکت از سیستم های توزیع شده بر روی سوپرکامپیوترهای گران قیمت به شبکه های بسیار پر قدرت و ارزان در مدت نسبتا کوتاهی صورت گرفته است. همچنین نیاز به مدیریت اطلاعات، پردازش، گردش کار و دیگر ابزار مدیریتی همواره رشد فزاینده داشته است. به طبع این نیاز، ساختار سیستم های کامپیوتری در سطوح فنی و مدیریتی نیز رشد کرده و پیچیده تر شده است.
به منظور جوابگویی به این حجم فزاینده درخواست ها و نیاز بازار به منابع پردازش و ذخیره سازی اطلاعات و نیز به منظور ارائه سرویس های مورد نیاز با کیفیت مناسب و قابل رقابت، یکی از بهترین راه های پیشنهاد شده، متمرکز نمودن این منابع و مدیریت صحیح آنها است. به این منظور و برای به حداکثر رساندن کیفیت خدمات و حداقل نمودن هزینه ها یکی از رایج ترین راهکارهای موجود راه اندازی مراکز داده یا دیتا سنتر ها می باشد. در این طرح با آماده سازی زیر ساخت های فیزیکی، امنیتی، شبکه ای، سخت افزاری و نرم افزاری، مجموعه ای از سرورهای قدرتمند برای ارائه سرویس های مورد نیاز مشتریان در نظر گرفته می شود. این سرورها با خطوط بسیار پر سرعت بر حسب نیاز به اینترنت یا شبکه های سازمانی متصل می گردند و با نصب سیستم های عامل و نرم افزارها و سرویس های مورد نیاز به کاربران خدمات لازم را ارائه می نمایند. با وجود چنین مراکزی دیگر سازمان ها و مراکز تجاری، صنعتی، دانشگاهی و غیره نیازی به راه اندازی مراکز سرویس دهی محلی[2] و نیز متحمل شدن هزینه های نگهداری، به روز رسانی و استخدام متخصصین نخواهند داشت. در ادامه به بررسی اجمالی دیتا سنترها خواهیم پرداخت تا بتوانیم طرح پیشنهادی را تشریح نمائیم.
تعریف دیتا سنتر: مجموعه ای از سیستمهای پشتیبانی (از جمله زیر ساخت سخت افزاری passive، زیرساخت خنک کننده، زیر ساخت تامین انرژی، اطفاء حریق و غیره)، منابع پردازشی سخت افزاری شامل سرورها، تجهیزات زیرساخت شبکه، زیرساخت ذخیره سازی داده ها و زیرساخت نرم افزاری شامل ابزار یک پارچه سازی[3]، مجموعه ای از سیستم های عامل، مجموعه ای از نرم افزارهای کاربردی شامل سرویس ها، تعدادی پایگاه داده، مجموعه ای از ابزارهای امنیتی نرم افزاری و سخت افزاری و یک ساختار مدیریتی است. این سیستم به کمک خطوط پرسرعت به شبکه های خارجی (Intranet، Extranet یا اینترنت) متصل است ]1[.
با توجه به رشد نیازها و احتیاج کاربران به انعطاف پذیری و تحمل خطای بالا در این مراکز پردازشی، در سال های اخیر تکنولوژی مجازی سازی[4] به عنوان پاسخی به این نیازها و بهترین شیوه یکپارچه سازی ارائه شده و بسیار رشد کرده است. در حقیقت، این تکنولوژی به عنوان لایه مدیریت نرم افزاری و سیستم عاملی دیتا سنتر مورد استفاده قرار می گیرد. در ادامه به تشریح تکنولوژی مجازی سازی و نحوه استفاده از آن در این طرح خواهیم پرداخت.
تکنولوژی مجازی سازی یکی از جوانترین نظریه های مطرح شده در علم کامپیوتر می باشد که در ده سال اخیر توجه زیادی را به خود جلب نموده است. این تکنولوژی از این بابت بسیار جذاب است که انعطاف پذیری و امکانات خارق العاده ای را بر روی همان بستر سخت افزاری موجود ارائه می دهد و استفاده از آن هزینه بسیار ناچیزی برای سازمان دارد.
معماری مجازی سازی، همه منابع پردازشی از جمله سرورها، منابع ذخیره سازی[5] و شبکه را به یک ساختار مجازی نگاشت می دهد. این زیر ساخت با گردآوری همه منابع و نمایش مجموعه ای ساده شده و یکپارچه از آنها، مدیر را در درک بهتر ساختار فنی دیتا سنتر و مدیریت و تغییر آن یاری می رساند. به کمک این ساختار می توان منابع توزیع شده در یک دیتا سنتر را به صورت مجموعه ای یکپارچه از ابزار مدیریت نمود. همچنین می توان از دیتا سنتر برای مصارف گوناگونی استفاده کرد بدون اینکه نگران گوناگونی سخت افزارها و نحوه اتصال آن ها به سیستم باشیم؛ ]2[ و ]3[.
از این تکنولوژی برای طراحی زیر ساخت نرم افزاری دیتا سنتر استفاده خواهد شد. با این توضیح که به جای نصب یک سیستم عامل بر روی هر دستگاه سرور، از یک نرم افزار مجازی سازی به نام Hypervisor استفاده می شود. این نرم افزار شبه سیستم عامل به مدیر سیستم اجازه می دهد که به تعداد دلخواه کامپیوتر مجازی[6] بر روی سرور مذکور راه اندازی کرده و سیستم عامل و سرویس های دلخواه را بر روی آن نصب نماید (شکل 1.1).
شکل 1.1. نحوه قرارگیری لایه های نرم افزاری بر روی سرور
با این ترکیب می توان امکانات بسیار زیادی از جمله قابلیت دسترسی دائمی به سرویس ها (HA)[7] و مقاوم سازی سرویس ها در مقابل خطا[8] که از ضروریات چنین دیتا سنتری می باشد را با کمترین هزینه میسر نمود. همچنین امکان انتقال این کامپیوترهای مجازی در حال کار از روی یک سرور به سرور دیگر را بدون تاخیر زمانی وجود دارد[9].
در دیتاسنتری با این ابعاد، اغلب سرویس های در حال کار بسیار حیاتی و حساس بوده و از کار افتادن آن ها هزینه های هنگفت و بعضا جبران ناپذیری برای سازمان مربوطه به دنبال خواهد داشت. به همین دلیل لازم است امکانات حرفه ای را در دیتا سنتر به منظور محافظت از سرویس ها پیاده سازی نمائیم تا در دسترس بودن و سلامت آنها را تضمین کند. شکل 1.2 شمایی کلی از یک دیتا سنتر را با استفاده از معماری یاد شده نشان می دهد.
شکل 1.2. شمای کلی دیتا سنتر با معماری مجازی
با توجه به نیاز به این مراکز و پیچیدگی ذاتی آنها، ترسیم یک مدل فرمال از ماهیت یک دیتا سنتر، چه پیش از طراحی[10] و چه پس از آن[11]، می تواند در شناخت طرز کار و چگونگی فعالیت چنین مرکزی نقش به سزایی داشته باشد. از جمله این کاربردها می توان به تشخیص بن بست ها[12] و گلوگاه ها[13] قبل از طراحی و محک زدن[14] سیستم بعد از طراحی اشاره نمود. با در دست داشتن این مدل (تصویر فرمال) جریان کنترل در سیستم قابل رویت بوده و در نتیجه رفتار سیستم را می توان بررسی و پیش بینی نمود ]4[. البته باید توجه داشت که در سیستم های واقعی از جمله دیتا سنترها، به دست آوردن مدل جامع تقریبا غیر ممکن بوده و تنها می توان بخش هایی از سیستم را با نادیده گرفتن برخی از پارامترها مدل نمود. هرچقدر مدل به سیستم واقعی نزدیکتر باشد بررسی رفتار سیستم به کمک مدل حاصل دقیقتر و کاربردی تر خواهد بود. در بخش های بعدی با بررسی دقیقتر ماهیت مدل سازی فرمال، با انواع شیوه ها در این حوزه[15] بیشتر آشنا خواهیم شد.
به طور کلی متد های فرمال نوع خاصی از شیوه های بیان فرمال مسائل هستند که از آنها برای تشریح و تبیین[16] سیستم های کامپیوتری و همچنین اثبات رفتار آنها[17] در سطح سخت افزار و نرم افزار استفاده می شود. هدف از توضیح رفتار یک سیستم به کمک روش های فرمال، بررسی رفتار و خصوصیات سیستم از جمله میزان حد پذیری[18]، بازگشت پذیری[19] و نیز پارامترهای انتزاعی تر مانند میزان ثبات[20] و پایداری[21] می باشد ]5[.
بدیهی است انجام چنین کاری در مورد سیستم های واقعی با توجه به پارامترهای متعدد و ساختار پیچیده آنها بسیار وقت گیر و دشوار است و در بسیاری از مواقع فقط بخش هایی از سیستم را می توان در حد قابل قبولی تشریح و مدل نمود. به همین دلیل و نیز به دلیل هزینه بسیار گزاف این فرایند، استفاده از شیوه های فرمال برای توضیح رفتار سیستم فقط در مورد سیستم های بسیار حساس و گران قیمت صورت می گیرد.
در این تحقیق، از زبان شبکه های پتری که ابزاری گرافیکی برای تشریح رفتار سیستم ها می باشد بهره گرفته شده است. این زبان در واقع نوع خاصی از ماشین های متناهی (اتوماتا) می باشد که امکان ترسیم جریان کنترل در سیستم را به صورت ساختار گراف و تعریف مجموعه ها فراهم می کند.
دامنه تحقیقدر این تحقیق، به کمک زبان فرمال شبکه های پتری، مدل فرمالی از بخش های مختلف یک دیتا سنتر نمونه ارائه خواهد شد. به این منظور در ابتدا ساختار دیتا سنترهای نوین شرح داده شده و سپس یک مدل کلی و انتزاعی برای آن ارائه می گردد.
در مراحل بعد، هریک از بخش های دیتا سنتر نمونه در لایه های بعدی طراحی و مدل خواهد شد. این بخش ها عبارتند از: سرویس HA ، سرویس Fault Tolerance، سرویس VMotion ، ساختار ESX، معماری سیستم ذخیره سازی در ESX، معماری شبکه در ESX و معماری سوئیچ مجازی در ساختار شبکه.
در انتهای هر بخش، مدل های پتری طراحی شده به کمک ابزار و متد های فرمال بررسی و ارزیابی خواهند شد. بخشی از این متدها مرتبط با نوع و گروه بندی شبکه هایی است که مدل مذکور در آن جای می گیرد، و بخشی نیز وابسته به خواص عمومی گراف ها می باشد.
پیشینه تحقیق
با توجه به قابلیت بسیار زیاد شبکه های پتری در مدل سازی سیستم های موازی، همگام، توزیع شده، غیرتعینی، و آماری، می توان نمونه های بسیاری از توصیف های فرمال سیستم های واقعی را به کمک این ابزار ذکر کرد. از آن جمله می توان به موارد زیر اشاره کرد.
طراحی مدل شبکه ترافیک شهری به کمک شبکه های پتری رنگی (سطح بالا) برای تخمین گلوگاه ها و نیز میزان کارامدی سیستم ترافیک ]6[.
مدل سازی فرمال یک خط اولید به همراه پنج ربات برای تحلیل خصوصیات رفتاری خط تولید و میزان خوش رفتاری آن ]7[
مدل سازی یک پردازنده مبتنی بر VLSI که در یک سوپر کامپیوتر به کار رفته است. این مدل سازی به کمک شبکه های پتری رنگی و در سطح رجیستر های این ریز تراشه انجام شده است.
در مرجع ]8[ می توانید لیست بلندی از سیستم های صنعتی مدل شده با شبکه های پتری را که به صورت پروژه های مجزا انجام شده مشاهده نمائید. با این حال در زمینه لایه نرم افزاری و مجازی سازی در دیتا سنترها و نیز بخش سیستم عاملی آن تا به حال مدل سازی جامعی به کمک شبکه های پتری انجام نشده است. هر چند تلاش هایی در زمینه مدل سازی زیر ساخت سخت افزاری دیتا سنتر و برای بهینه نمودن مصرف انرژی در آنها و طراحی دیتا سنترهای سبز (دوستدار محیط زیست) با شبکه های پتری انجام شده است.]9[
اهداف تحقیقتشریح ساختار نرم افزاری دیتا سنترهای نوین
تشریح ماهیت و مکانیزم های مجازی سازی، فواید و کاربرد های آن و نحوه طراحی دیتا سنتر به کمک این تکنولوژی
ارائه مدل های فرمال از ساختار های پیشنهاد شده در بخش های نرم افزاری دیتا سنتر بر روی پلتفورم مجازی.
ارائه تحلیل و اثبات خواص رفتاری سیستم بر روی مدل های طراحی شده.
سوالات تحقیقموارد زیر می تواند بخشی از سوالاتی باشد که در این تحقیق مطرح می شوند:
ساختار سیستم عاملی و نرم افزاری یک دیتا سنتر چگونه است؟
تکنولوژی مجازی سازی چگونه در ساختار نرم افزاری دیتا سنتر ترکیب می شود و کار می کند؟
چگونه می توان یک تصویر فرمال از یک دیتا سنتر نمونه که بر مبنای تکنولوژی گفته شده طراحی شده است را به دست آورد؟
چه دانشی می توان از مدل فرمال طراحی شده استخراج نمود؟
مراحل و روش تحقیقبا توجه به اینکه مرحله نهایی در تحقیق، رسیدن به مدل هایی فرمال است که ساختار داخلی سیستم و رفتار آن را به روشنی نشان دهد، باید در ابتدا مقدماتی از جمله مبانی نظری دیتا سنترها، مجازی سازی و نیز ابزار فرمال برای مدل سازی سیستم ها مطرح و تشریح گردد.
با این رویکرد، پس از تشریح ابزار فرمال و نیز انواع تکنولوژی های مورد استفاده در دیتا سنتر، با ترکیب این دو حوزه، به بررسی و تشریح ساختار داخلی و نحوه رفتار دیتا سنترها به کمک ابزار و زبان های مورد استفاده می پردازیم. در این مسیر دنبال کردن سوالات و بخش های زیر راهگشا خواهد بود:
مدل سازی چیست و ابزار فرمال برای این کار چه هستند؟
مدل سازی فرمال یک سیستم چه امکاناتی در اختیار ما قرار می دهد و دانش قابل استخراج از آن چیست؟
دیتا سنترهای امروزی از چه بخش هایی تشکیل شده اند و چگونه قابل تجزیه هستند؟
چگونه می توان به شیوه سلسله مراتبی، مدل های فرمالی از بخش های سیستم از کل به جزء طراحی نمود؟
در پایان با ارزیابی مدل های تهیه شده، می توان به ارزیابی از میزان خطاپذیری و نقاط ضعف سیستم دست یافت.
در اینجا ذکر این نکته ضروری است که در مدل سازی فرمال لایه مجازی سازی در سیستم های پردازشی، آنگونه که در این تحقیق به آن پرداخته شده، تحقیقات بسیار اندکی انجام شده است. از این رو بخش های زیادی در مورد پیشینه تحقیق به چشم نمی خورد.
دستاوردهای تحقیقحاصل کار این تحقیق، مدل های فرمال متعددی از بخش های نرم افزاری یک دیتا سنتر نمونه است. این مدل ها می توانند در شناخت ضعف ها، ناکارآمدی ها و گلوگاه های سیستم نقشی فعال و محسوس بازی نماید. همچنین به کمک این مدل در زمان طراحی سیستم شناخت دقیقتری نسبت به کارکرد و رفتار آنها حاصل خواهد شد و همین امر به طراحی یک سیستم پایدار و دقیق کمک شایانی می نماید.
نگاهی کلی بر پایان نامهاین پایان نامه از بخش های زیر تشکیل شده است:
فصل دوم: بررسی و مقایسه زبان های فرمال برای مدل سازی، توصیف و بررسی سیستم های موازی، غیر همگام[22]، توزیع شده، غیر قطعی[23]، آماری[24] و دینامیک. در این بخش توانایی ها و قابلیت های این ابزار با یکدیگر مقایسه و در نهایت یکی از آنها برای استفاده در بخش های بعد انتخاب می گردد.
فصل سوم: بررسی زیرساخت نرم افزاری دیتا سنتر بر مبنای تکنولوژی مجازی سازی. در این بخش همچنین امکانات و قابلیت های استفاده از این تکنولوژی در طراحی معماری دیتا سنتر مورد بررسی و تشریح قرار می گیرد.
فصل چهارم: ارائه مدل از بخش های مختلف معماری نرم افزاری دیتا سنتر و تحلیل مدل. در این بخش پس از طراحی مدل پتری هریک از ماژول ها، با تحلیل فرمال مدل متناظر، خصوصیات رفتاری مختلفی از آنها بررسی و اثبات می شوند.
فصل دوم: مروری بر ابزار فرمال مدل سازی سیستم ها
طبق آمار سایت های غیر رسمی[25] در حدود 100 متد فرمال به صورت زبان، notation و ابزار وجود دارد که به منظور تشریح فرمال سیستم ها و مسائل از آنها استفاده می شود. پارامترهای زیادی وجود دارد که نقاط قوت و ضعف هر یک از ابزار مذکور را نسبت به دیگران تعیین می نماید اما در این بین تعدادی از این مصادیق به دلایلی عمومیت بیشتری یافته اند و بیشتر در مورد بررسی و به روز رسانی قرار گرفته اند.
به طور کلی می توان ابزار توصیف فرمال[26] را به دو گروه متدهای جبری و متدهای مبتنی بر مدل تقسیم بندی نمود ]5[ و ]10[. اگر فرض نمائیم که بهترین شیوه شناخت و توصیف سیستم ها شکستن آنها به بخش های کوچکتر و ساده تر[27] برای کنترل پیچیدگی سیستم است، از بررسی شیوه توصیف هریک از این دو نوع ابزار می توان نتیجه گرفت که متدهای جبری برای توصیف interface بین بخش های سیستم مذکور مناسب است زیرا خصوصیات کارکردی[28] یا ساختاری[29] سیستم را به نحو مطلوبی نشان می دهد. با این حال این ابزار برای تشریح رفتار سیستم چندان کارآمد نیست. به منظور توصیف خصوصیات رفتاری یک سیستم[30] از ابزار مدل سازی فرمال استفاده می گردد. در شکل 2.1 مثالهایی از گروه های گفته شده و نیز تقسیم بندی توانایی آنها در تشریح سیستم های تسلسلی[31] و موازی[32] آورده شده است.
شکل 2.1. مثال هایی از زبان های فرمال و تقسیم بندی آنها ]10[
به طور کلی استفاده از توصیف فرمال سیستم ها قبل از طراحی و پیاده سازی، همراه با مشکلاتی مانند هزینه بر بودن، زمان بر بودن و نیز دشواری و پیچیدگی در بیان و ارزیابی آن است. این موانع باعث شده است تا این شیوه توسعه برخلاف آنچه که در دهه 1980 پیش بینی می شد، پرکاربرد ترین شیوه توسعه سیستم های نرم افزاری و سخت افزاری نشود. با این حال مزایای این روش پیاده سازی که کاهش محسوس خطاهای سیستم در هنگام طراحی و پیاده سازی است باعث شده است که در طراحی سیستم های حیاتی و گران قیمت مورد استفاده قرار گیرد.
با توجه به اینکه توصیف یک سیستم به شکل تفکیک ناپذیری در طراحی آن گره خورده است، می توان برای طراحی سیستم به شیوه توصیف فرمال آن، روالی طبق شکل 2.2 را مد نظر قرار داد.
شکل 2.2. روال طراحی یک سیستم نمونه به کمک متد های فرمال ]10[
همانگونه که دیده می شود، برقراری درک دقیقی از نیازمندیهای سیستم[33] ، طراحی معماری و نیز توصیف (درک) فرمال سیستم به شکلی با یکدیگر ادغام شده اند که بازخورد هر مرحله از توصیف به کامل تر شدن طراحی در همان مرحله کمک می کند. بنابراین در پایان فاز توصیف فرمال، حداقل میزان خطا و حالات پیش بینی نشده در سیستم وجود خواهد داشت. درصد این خطا مستقیما به میزان توانایی ابزار توصیف در بررسی و تبیین جنبه های مختلف کارکردی و رفتاری سیستم باز می گردد ]11[.
در ادامه سعی می کنیم تعدادی از این ابزار فرمال را تشریح کرده و با هم مقایسه نمائیم. بعضی از نمونه ها تنها به صورت متد بوده و بعضی دیگر دارای گرامر نیز می باشند و زبان هستند.
ASM
ASM[34] از ساختارهای کلاسیک ریاضی برای توصیف فرمال سیستم استفاده می کند بنابراین بسیار دقیق است. با این توضیح که ASM متدی مبتنی بر جبر رابطه ای و مناسب برای توصیف سیستم های تسلسلی است. باید توجه داشت که اگر در توصیف مسائل، semantic متد به کار رفته مبهم باشد توصیف حاصل واضح تر از تعریف اولیه سیستم نخواهد بود. بنابراین ASM با یک تعریف ریاضی، وضوح و یگانگی درک مفهوم مورد نظر را تضمین می کند[35]. ASM شکل خاصی از finite-state automata است که از مجموعه ای از ساختار های داده ای[36] و توابع ریاضی تشکیل شده است و برای توصیف الگوریتم ها بر اساس حالات[37] آنها به کار می رود ]12[.
در واقع ASM یک ساختار قراردادی ساده یا پیچیده از قواعد ریاضی است که از مجموعه ای از دامنه ها (یا مجموعه ها که هر یک نوع مشخصی از اشیا را نشان می دهند) و توابع و روابط قراردادی بر روی آنها تعریف شده اند ]13[. همانگونه که دیده می شود این مجموعه بسیار انتزاعی و مستقل از نوع مساله است.
دستیابی به سطوح بالایی از انتزاع از مهمترین مزایای ASM است.
در ادامه نمونه از تعریف فرمال ASM را برای سیستم PVM[38] مشاهده می کنیم ]12[:
master : HOST
مشخص کننده ی ماشینی است که PVM روی آن اجرا می شود و و نقش کلیدی در مدیریت و نگهداری پیکره پویای PVM دارد.
arch : HOST → ARCH
تابع arch که معماری هر یک از HOSTها را مشخص می کند. این معماری عضوی از مجموعه انتزاعی ARCH است.
daemon : HOST → DAEMON
این تابع برای هر عضو از مجموعه HOST، پروسه ای از مجموعه DAEMON را مشخص می کند که وظیفه مدیریت برنامه های آن هاست و نیز ارتباطات بین پروسه ها را برعهده دارد. این daemon به کمک مجموعه ای از پروسه ها بر روی host پیاده سازی می شود.
demiurge : DAEMON
daemon خاصی است که بر روی master host اجرا می شود (می توان آنرا به صورت daemon(master) = demiurge بیان کرد) و وظیفه آن ایجاد و حذف hostها و نگهداری ارتباطات آنهاست.
این اشیا و روابط انتزاعی مقدمه ای برای مدل ASM از VPM است. در حال حاضر اطلاعات بیشتری در مورد ماهیت hostها، daemonها و معماری آنها مورد نیاز نیست.
در این زبان می توان از سودوکدهای ساده استفاده نمود بنابراین نحو[39] زبان برای اکثر افراد قابل درک است.
بر خلاف بسیاری از ابزار، می توان مدل طرح شده به ASM را مستقیما اجرا نمود تا نتیجه رفتار سیستم مشخص گردد. همچنین از این ابزار می توان برای مدل کردن طیف وسیعی از سیستم ها استفاده کرد. از جمله می توان به سیستم های تسلسلی، موازی، توزیع شده، real time، سیستم های متناهی و نامتناهی و غیره اشاره نمود که نشان دهنده انعطاف پذیری ابزار می باشد.
در ادامه نمونه ای از نحو زبان ASM آورده شده است. این بخش چگونگی انتقال پیام مابین Agent ها را نشان می دهد. ]14[.
class COMMUNICATOR
Program() =
let availableMsgs = {m | m in me.mailbox where ReadyToDeliver(m)}
let selectedMsgs = chooseSubset(availableMsgs)
forall msg in selectedMsgs
me.mailbox(msg) := false //delete the message
let resolvedMsgs = ResolveMessage(msg) //resolve the message
forall m in resolvedMsgs
let a = Recipient(m)
if a <> undef then // if recipient found
InsertMessage(a,m) // forward the message
else
skip // else ignore message
برای مطالعه بیشتر به ]29[ الی ]32[ مراجعه کنید.
LOTOS
LOTOS[40] توسط سازمان ISO برای بیان فرمال استاندارد های مربوط به OSI ساخته شد. این زبان به عنوان به عنوان یک FDT[41] تحت استاندارد ISO/IEC 8807 در سال 1989 ارائه گردید[42].
LOTOS یک زبان توصیف فرمال مبتنی بر روابط جبری است که برای توصیف سیستم های موازی و توزیع شده مناسب می باشد ]15[. در واقع دو بخش اصلی تشکیل دهنده LOTOS عبارتست از ADT[43] و جبر پروسه ها. به دلیل پشتیبانی از گونه های داده ای انتزاعی، این زبان می تواند تبادل اطلاعات و در نتیجه رابطه بین اجرا را به خوبی توصیف نماید. همچنین به دلیل جبری بودن، خواص عملکردی سیستم را توصیف می نماید. به علاوه، پشتیبانی از عملگرهای –poral باعث می شود که این زبان توانایی توصیف خواص رفتاری و جنبه های زمانی سیستم ها را نیز داشته باشد.
مقدمه ای بر جبر پروسه ها[44] ]16[
در این جبر، اجزای سیستم به صورت پروسه های انتزاعی نمایش داده می شوند که با یکدیگر ارتباط دارند. پروسه ها به صورت جعبه سیاه دیده می شوند که تنها رفتار خارجی آنها مورد بررسی قرار می گیرد. همچنین پروسه ها به کمک مکانیزم interaction point با یکدیگر رابطه برقرار می کنند. در LOTOS به این نقاط event gate یا به اختصار gate گفته می شود (شکل 2.3).
شکل 2.3. نقطه gate در جبر پروسه ها ]4[
Event نشان دهنده یک همگامی[45] بین دو یا چند پروسه است. به طور کلی سه نوع event تعریف شده اند:
Pure synchronization: هیچ مقداری بین پروسه ها تبادل نمی شود.
Value establishment: مقادیر ارائه شده توسط یک یا چند پروسه از سوی بقیه مورد پذیرش نیست.
Value negotiation: مقادیر از سوی یک یا چند پروسه مورد قبول است.
همچنین یک عبارت رفتاری[46] انتخابی از بین مجموعه ای از event ها است که برای یک محیط مطرح می گردد. در شرایطی که امکان همگام سازی بین eventهای پیشنهاد شده در یک محیط وجود نداشته باشد یک بن بست[47] رخ داده است. همچنین اگر هیچ پیشنهادی در محیط مطرح نشده باشد یک livelock رخ می دهد (مانند یک حلقه بینهایت).
همچنین LOTOS مفهوم ترتیب زمانی eventها را نیز به قواعد جبری موجود اضافه نموده است. این زبان از عملگرهای –poral برای ترکیب عبارات رفتاری و به دست آوردن عبارات رفتاری پیچیده تر استفاده می کند. در عین حال این عملگرها از قواعد خوش تعریف پیروی می نمایند که تفسیر صریح و یکسانی را برای افراد ممکن می سازد.
به عنوان خلاصه ای از خصوصیات LOTOS، می توان آنرا تعریف فرمالی از ترکیب داده و کنترل، بر مبنای جبر پروسه ها دانست که همزمانی[48] یکی خصوصیات ذاتی آن است. همچنین قواعد LOTOS به دلیل عملیاتی بودن قابل تفسیر و اجرا[49] می باشد و ماژولار است ]17[.
در ادامه مثالی از مدلسازی مساله تولید کننده- مصرف کننده[50] با این زبان آورده شده است. در این مساله سه ماژول تولید کننده، مصرف کننده و کانال که وظیفه هماهنگ سازی این دو را به عهده دارد حضور دارند. لازم به ذکر است که تغییراتی در صورت مساله به وجود آمده تا خصوصیات LOTOS بهتر نشان داده شود. ازآن جمله، تولید کننده می تواند دو خروجی را به صورت همزمان یا غیر همزمان تولید نماید و سپس متوقف شود. همچنین مصرف کننده پس از مصرف ترتیبی یا همزمان آنها متوقف می گردد (شکل 2.4).
شکل 2.4. مدل تولید کننده- مصرف کننده به کمک LOTOS ]17[
برای کنترل پیچیدگی مساله، در ابتدا عمل تجزیه[51] را روی این سه بخش انجام داده و هر یک را به عنوان یک پروسه مستقل تشریح می کنیم. سپس آنرا را با هم ترکیب می نمائیم.
با توجه به تعاریف pc1 و pc2 به عنوان کانال های تولید کننده و cc1 و cc2 به عنوان کانال های مصرف کننده و همچنین عملگرهای انتخاب ([]) و فعال سازی[52] (>>) می توان پروسه های فوق را به صورت زیر تعریف نمود:
پروسه تولید کننده:
process Producer [pc1, pc2] : exit :=
pc1; pc2; exit
endproc
پروسه کانال:
process Channel [ pc1, pc2, cc1, cc2] : exit :=
pc1;
(
pc2; cc1; exit
[]
cc1; pc2; exit
)
>> cc2; exit
endproc
پروسه مصرف کننده:
process Consumer [cc1, cc2] : exit :=
cc1; cc2; exit
endproc
در این بین می توان جزئیات اجرایی بیشتر مانند عملکرد داخلی هریک از پروسه ها را با عملگرهای بیشتری مدل نمود به عنوان مثال مساله گم شدن یکی از ورودی ها به کانال به شکل زیر قابل توصیف است:
process Channel [pc1, pc2, cc1, cc2] : exit :=
pc1; ( pc2 ; cc1; exit [] cc1; pc2; exit [] i; pc2; exit )
>> ( cc2; exit [] i; exit)
Endproc
در نهایت با تعریف عملگر میانه گزاری[53] (|||) برای شبیه سازی توازی[54] بین پروسه ها می توان ترکیب سه پروسه یاد شده را به شکل زیر نوشت:
specification Producer_Consumer [ pc1, pc2, cc1 cc2 ] : exit
behavior
(
Producer [ pc1, pc2 ]
|||
Consumer [ cc1, cc2 ]
)
||
Channel [pc1, pc2, cc1, cc2]
where
process Producer [ out1, out2 ] : exit := . . . (*As defined previously*)
process Consumer [ in1, in2 ] : exit := . . . (*As defined previously *)
process Channel [ le1, le2, , re1, re2 ] : exit := . . . (*As defined previously *)
endspec
برای جزئیات بیشتر در مورد مثال فوق و عملگرهای زبان LOTOS به ]17[ و برای مطالعه بیشتر در مورد زبان LOTOS به ]33[ الی ]34[ مراجعه کنید.
VDM-SL
VDM-SL[55] ابزاری برای توصیف مسائل نرم افزاری است که به صورت مجرد و مستقل از جزییات ماشین ابداع شده است. با توجه به اینکه VDM یک زبان بوده و دارای semantic فرمال می‌باشد، ابزای برای ارزیابی آن نیز ارایه شده است که می‌توان الگوریتم های مدل شده در این زبان را ارزیابی نمود. همچنین ابزاری برای اجرای سیستم مدل شده و مشاهده نتیجه تست برای آن پیش‌بینی شده تا کسانی که با VDM آشنایی ندارند بتوانند سیستم مورد نظر خود را بررسی کنند.
با این حال این زبان قابلیت مدل سازی سیستمهای موازی را ندارد.
با توجه یه اینکه VDM یک زبان model-based است به طور کلی تفاوت بین این گروه از ابزار فرمال و متدهای جبری را می توان اینگونه توضیح داد که در گروه اول، ما عملیات در یک سیستم را بر اساس اینکه چه تأثیری بر مقادیر می گزارند توصیف می کنیم. در مقابل در ابزار جبری، خصوصیات عملیات را به صورت مجرد شرح می دهیم ]18[.
با توجه به اینکه بیشترین توان VDM در مدل سازی سیستم های خطی است، به نظر می رسد این زبان بیشتر به توصیف خصوصیات کارکردی سیستم می پردازد. بنابراین بخش بزرگی از توصیف به بیان انواع داده‌ای ساده و مجرد و نیز ADT ها مربوط است. در چنین حالتی بسیاری از ساختار های عبارات جبری قابل نگاشت به این زبان هستند.
در ادامه مدل ساده‌ای از VDM برای مدل سازی حساب بانکی آورده شده است ]18[:
در این مثال مشتری با CustNum و حساب با AccNum مدل می شود.
AccNum = token;
CustNum = token;
Balance = int;
Overdraft = nat;
AccData :: owner : CustNum
balance : Balance
state Bank of
accountMap : map AccNum to AccData
overdraftMap : map CustNum to Overdraft
inv mk_Bank(accountMap,overdraftMap) == for all a in set rng accountMap & a.owner in set dom overdraftMap and
a.balance >= -overdraftMap(a.owner)
برای مطالعه بیشتر به ]35[ الی ]36[ مراجعه کنید.
شبکه های پتری
شبکه های پتری[56] یکی از قدیمیترین زبان های فرمال برای توصیف و ارزیابی سیستم ها است. از بارزترین خصوصیات این زبان می توان به توانایی آن برای توصیف سیستم های موازی اشاره نمود. همچنین به دلیل پختگی[57]، این زبان مکانیزم هایی برای بیان جنبه های کارکردی و رفتاری سیستم ارائه می نماید. همچنین علاوه بر توانایی توصیف سیستم ها، می تواند شیوه هایی برای تحلیل[58] و ارزیابی[59] و نیز در نهایت اثبات فرمال آنها[60] ارائه نماید ]19[ الی ]22[.
بر اساس تعریف، یک شبکه پتری به صورت زیر به شکل فرمال تعریف می شود ]23[:
مجموعه متناهی از موقعیت ها[61]
مجموعه متناهی از گزارها[62]
مجموعه ای از لبه های گراف[63] (روابط بین pها و tها)
W: {1, 2, 3, …}
تابع وزن گذاری روابط
وضعیت اولیه سیستم.
همچنین ضروری است :
به عنوان مثال مدل ساده ای از یک پروتکل ارتباطی در شکل 2.5 نشان داده شده است.
شکل 2.5. مثالی از مدل سازی یک پروتکل به کمک شبکه های پتری ]23[
در شکل بالا، وضعیت شروع = (1,0,0,1,0,0,0,0) می باشد که به معنی فعال بودن موقعیت های p1 و p4 است. بنابراین گزارهای t1 و t5 به ترتیب فعال[64] هستند. باید توجه داشت که فعال بودن یک گزار لزوما به معنی اجرا شدن[65] آن نیست بلکه اجرا شدن به رخ دادن اتفاق در سیستم واقعی بر می گردد. همچنین اجرا شدن t1 و t5 به ترتیب توکن های p1 و p4 را حذف کرده و توکن هایی به p2 و p5 اضافه می کند.
خصوصیات رفتاری[66]
با تعریف وضعیت شروع[67] به عنوان وضعیت اولیه سیستم ، خصوصیات رفتاری در واقع جنبه هایی از سیستم هستند که به این وضعیت شروع وابسته هستند و در موقعیت های اجرایی سیستم تغییر می کنند.
در شبکه (N, M0) (شبکه پتری N با وضعیت شروع )، مجموعه تمام دنباله های گزارهای قابل اجرا که از وضعیت M0 شروع می شوند را با L(N, M0) و یا به شکل ساده تر با L(M0)[68] نشان می دهند.
به کمک پارامترهای زیر می توان جنبه های رفتاری سیستم توصیف نمود ]23[ و ]24[:
Reachability
طبق تعریف، وضعیت سیستم در ، از وضعیت ، reachable خواهد بود اگر دنباله ای از اجرای گزارها[69] وجود داشته باشد که را به ببرد.
مجموعه وضعیت های قابل دسترسی از طریق را با مجموعه نشان میدهیم.
Boundedness
شبکه پتری (N,)، k-bounded یا به اختصار bounded خواهد بود اگر تعداد توکن های موجود در هر place، برای همه وضعیت های قابل دستیابی از وضعیت شروع، از تعداد محدود k تجاوز نکند. به عبارت دیگر .
همچنین یک شبکه پتری 1-bounded، شبکه پتری ایمن[70] نامیده می شود.
Liveness
این مفهوم در ارتباط نزدیک با مفهوم عدم وجود بن بست در سیستم عامل ها می باشد. شبکه پتری (N,)، live خوانده می شود (به عبارت دیگر وضعیت یک وضعیت live برای N شمرده می شود) اگر، بدون توجه به اینکه چه وضعیتی از پیش می آید، در نهایت اجرای تمام گزارهای شبکه با دنبال کردن دنباله ای از گزارها ممکن باشد.
این بدان معنی است که یک شبکه پتری live عملیات بدون بن بست را تضمین می کند بدون اینکه ترتیب اجرای گزارها مهم باشد. به عنوان نمونه، شبکه شکل 2.6 دارای خصوصیت Liveness نمی باشد زیرا در صورتی که گزار t1 در ابتدا اجرا شود، دیگر هیچ یک از گزارها امکان اجرا شدن نخواهند داشت.
شکل 2.6. نمونه ای از شبکه پتری non-Live ]23[
Liveness خصوصیتی ایده آل برای بسیاری از سیستم ها است. با این حال اثبات و فراهم کردن کامل این خصوصیت دشوار برای بسیاری از سیستم های پیچیده غیر ممکن و هزینه بر است. سیستم عامل کامپیوترهای بزرگ نمونه ای از چنین سیستم هایی است. بنابراین در عمل این خصوصیت نادیده گرفته شده و چندین سطح از Liveness برای شبکه ها در نظر گرفته می شود. بر این اساس سطح Liveness گزار t در شبکه پتری (N,) یکی از موارد زیر خواهد بود:
Dead (L0-live)
اگر t هیچ گاه و در هیچ یک از دنباله های اجرای L(M0) اجرا نشود.
L1-live (probably fireable)
اگر t حداقل یک بار و در یکی از دنباله های اجرای L(M0) بتواند اجرا شود.
L2-live
اگر با در نظر گرفتن عدد مثبت k، گزار t بتواند حداقل k بار در دنباله های اجرای مختلف L(M0) اجرا شود.
L3-live
اگر t به دفعات نامحدودی در تعدادی از دنباله های اجرای L(M0) ظاهر شود.
L4-live (Live)
اگر t در هر وضعیت M در R(M0) در مرتبه L1-live باشد.
■
گفته می شود شبکه پتری (N,)، Lk-live است اگر همه گزارهای موجود در شبکه حداقل از مرتبه Lk-live باشند و k=0,1,2,3,4. همچنین L4-liveness قویترین سطح live بودن سیستم و و معادل مفهومی است که در ابتدای بخش توضیح داده شد.
به سادگی می توان دریافت که یک گزار یا شبکه که در سطح k، live است، لزوما در سطح k-1 نیز live خواهد بود. به عبارت دیگر رابطه دلالت بین آنها به این شکل برقرار است:
L4-liveness => L3-liveness => L2-liveness => L1-liveness
گفته می شود گه یک گزار دقیقا Lk-live است اگر این گزار Lk-live باشد ولی L(k+1)-live نباشد، K=1,2,3.
Reversibility
شبکه (N,)، reversible است اگر برای هر وضعیت M، از طریق M قابل دستیابی (reachable) باشد.
Coverability
در شبکه (N,) گفته می شود وضعیت M قابل پوشش است اگر وضعیت در وجود داشته باشد به طوری که .
Home state
وضعیت در شبکه (N,)، Home state نامیده می شود اگر برای هر وضعیت M در ، از M قابل دسترسی باشد.
زیر مجموعه های شبکه های پتری
تعریف: یک شبکه پتری، شبکه اولیه[71] نامیده می شود در صورتی که وزن تمام لبه های آن 1 باشد.
با این تعریف در این بخش شبکه های اولیه ای را معرفی می کنیم که دارای خواص مشترکی هستند. البته باید توجه داشت که شبکه های اولیه و غیر اولیه هر دو دارای قدرت مدلسازی یکسانی هستند و تفاوت آنها در راحتی و سرعت استخراج و اثبات خصوصیات است. در این بخش از نشانه گذاری زیر به عنوان مقدمه استفاده می کنیم. در اینجا F مجموعه همه لبه های شبکه پتری است:
•t= {p| (p,t) F}
مجموعه موقعیت های ورودی به t
t•= {p| (t,p) F}
مجموعه موقعیت های خروجی از t
•p= {t| (t,p)F}
مجموعه گزارهای ورودی به p
p•= {t| (p,t)F}
مجموعه گزارهای خروجی از p
مثال هایی از نشانه های گفته شده در شکل 2.7 نشان داده شده است. با این تعریف می توانیم زیر مجموعه های شبکه های پتری را با اعمال قوانینی در ساختار آنها مشخص کنیم. در این تحقیق فرض شده است که در هیچ یک از شبکه های مورد بحث، موقعیت یا گزار ایزوله وجود ندارد یعنی گزار یا موقعیتی با شرایط •p= p•= Ø یا •t= t•= Ø وجود ندارد.
شکل 2.7. نشانه گزاری برای: a) مجموعه موقعیت های ورودی و خروجی برای t و b) مجموعه گزارهای ورودی و خروجی برای p ]23[
با مقدمه گفته شده، کلاس های زیر را برای شبکه های پتری داریم:
State Machine (SM)
یک شبکه پتری اولیه با این شرط که هر گزار t دقیقا یک موقعیت ورودی و یک موقعیت خروجی داشته باشد. یعنی:
|•t| = |t•| = 1for all t T.
Marked Graph (MG)
یک شبکه پتری اولیه با این شرط که هر موقعیت p دقیقا یک گزار ورودی و یک گزار خروجی داشته باشد. یعنی:
|•p| = |p•| = 1for all p P.
Free-choice net (FC)
یک شبکه پتری اولیه است که در آن هر لبه متصل به یک موقعیت، یا یک لبه خروجی یکتا از یک گزار و یا یک لبه ورودی یکتا به یک گزار است. یعنی:
For all , |p•| 1 or •(p•) = {p}
که معادل است با:
For all
Extended Free-choice net (EFC)
یک شبکه پتری اولیه است که:
for all
Asymmetric choice net (AC)
این کلاس که به عنوان شبکه ساده[72] هم شناخته می شود، یک شبکه پتری اولیه است که :
for all .
مثال هایی از کلاس های تشریح شده که تفاوت های کلیدی این زیر مجموعه های شبکه پتری را نشان می دهد در شکل 2.8 آمده است.
شکل 2.8. مثال هایی از زیر مجموعه های شبکه های پتری ]23[
قضایا و فرضیات ]23[
با یادآوری این نکته که شبکه اولیه به شبکه ای گفته می شود که وزن همه لبه های آن 1 باشد، قضیه های زیر را داریم:
قضیه 1: اگر شبکه پتری عادی (N, )، Live و Safe باشد، نباید در آن موقعیت source یا sink و نیز گزار source یا sink وجود داشته باشد یعنی: .
□
با بسط دادن این قضیه می توان گفت اگر شبکه پتری متصل (N, )، live و safe باشد، آنگاه شبکه N یک شبکه متصل قوی[73] است.
قضیه 2: اگر درخت پوشای شبکه پتری (N, ) را به عنوان T در نظر بگیریم، شبکه (N,)، Safe خواهد بود اگر و تنها اگر فقط مقادیر 0 و 1 در برچسب لبه های T وجود داشته باشد.
□
قضیه 3: اگر درخت پوشای شبکه پتری (N, ) را به عنوان T در نظر بگیریم، گزار t یک بن بست[74] است اگر و تنها اگر t به عنوان برچسب یک لبه در T ظاهر نشود.
□
قضیه 4: یک state machine، (N, )، live است اگر و تنها اگر این شبکه متصل قوی بوده و M0 حداقل یک توکن داشته باشد.
□
قضیه 5: یک state machine، (N,)، safe است اگر و تنها اگر M0 حداکثر یک توکن داشته باشد. همچنین شرط لازم و کافی برای اینکه یک live state machine، (N, )، safe نیز باشد این است که M0 دقیقا یک توکن داشته باشد.
□
در شبکه های marked graph، هر موقعیت دقیقا یک لبه ورودی و یک لبه خروجی با وزن واحد دارد. بنابراین گراف نشانه دار (N,) را می توان با گراف نشانه دار جهت دار[75] (G, ) نشان داد که در آن لبه ها معادل موقعیت ها و گره ها معادل گزارها هستند. شکل 2.9 مثالی از مدل پتری یک پروتکل ارتباطی در شبکه های کامپیوتری (الف) و گراف نشانه دار متناظر با آن (ب) را نشان می دهد.
شکل 2.9. یک شبکه پتری و گراف نشانه دار مربوط به آن ]23[
اجرای یک گره (گزار) در یک marked graph شامل حذف شدن یک توکن از از لبه های ورودی (موقعیت های ورودی) و اضافه شدن یک توکن به لبه های خروجی (موقعیت های خروجی) می باشد. اگر یک گره بر روی یک مدار جهت دار[76] یا حلقه قرار داشته باشد، آنگاه دقیقا یکی از لبه های ورودی و یکی از لبه های خروجی آن متعلق به حلقه مذکور خواهد بود. متقابلا، اگر گره ای بر روی یک حلقه قرار نداشته باشد، هیچ یک از لبه های متصل به آن متعلق به مدار جهت دار مذکور نخواهد بود.
با توجه به مقدمه گفته شده، قضایای زیر را در مورد خصوصیات نامتغیر[77] توکن ها در marked graph داریم:
قضیه 6: در یک marked graph، تعداد توکن ها در یک مدار جهت دار تحت اجرای هر گزاری، نا متغیر است؛ یعنی برای هر مدار جهت دار C و هر وضعیت M در R(M0) داریم:
M(C) = M0(C)
که در اینجا M(C) نشان دهنده مجموع تعداد توکن ها در C است.
□
بر اساس قضیه 6، اگر در وضعیت اولیه شبکه، توکنی در یک مدار جهت دار وجود نداشته باشد، این حلقه بدون توکن باقی خواهد ماند. بنابراین هیچ یک از گره ها (گزار) در آن امکان اجرا شدن نخواهند داشت. از سوی دیگر اگر یک گره هیچ گاه طی هیچ وضعیتی امکان اجرا شدن نداشته باشد (L0-live transition)، می توان با بررسی معکوس دنباله گزارها، مدار مستقیم بدون توکن را پیدا کرد. بر این اساس قضیه 7 را داریم:
قضیه 7: گراف نشانه دار (G, )، live است اگر و تنها اگر در وضعیت M0، حداقل یک توکن در هریک از مدارهای جهت دار G وجود داشته باشد.
□
قضیه 8: گراف نشانه دار live (G, )، safe خواهد بود اگر و تنها اگر هر لبه ای (موقعیت) در این گراف متعلق به مدار جهت دار C باشد به طوری که M0(C) = 1 .
□
لم 1: با استفاده از گراف پوشای مدل پتری (N,M0) تعدادی از خصوصیات آن را می توان بررسی نمود. از آن جمله می توان به موارد زیر اشاره کرد:
شبکه (N,M0) ، bounded و در نتیجه R(M0) متناهی است اگر و تنها اگر مقدار (تعداد بی نهایت توکن در یک موقعیت) در هیچ یک از برچسب های گره های گراف وجود نداشته باشد.
شبکه (N,M0)، safe است اگر و تنها اگر فقط مقادیر 0 و 1 در برچسب گره های گراف دیده شود.
گزار t در شبکه (N,M0) ، dead خواهد بود اگر و تنها اگر این گزار به صورت برچسب یک لبه در گراف پوشا ظاهر نشود.
اگر وضعیت M از طریق M0 قابل دسترسی (reachable) باشد. آنگاه در گراف گره ای با برچسب وجود دارد به طوری که
□
برای مطالعه بیشتر قضایا و فرضیات به ]25[ الی ]28[ مراجعه کنید.
جمع بندی
در فصل دو، با تکیه بر مطالعات انجام شده در زمینه ابزار توصیف فرمال سیستم ها، چهار ابزار مختلف را انتخاب و بررسی نمودیم. هر یک از این چهار ابزار، خواه مبنی بر ابزار ریاضی مانند گراف باشند و یا مبتنی بر روابط جبری، به طراح در به دست آوردن تصویری قابل درک از سیستم واقعی کمک می کنند. این تصویر می تواند با متد های قابل دفاع مورد بررسی و تحلیل قرار گرفته و ظرفیت ها و مشکلات سیستم را از جنبه های زیادی به طراح نشان دهد.
با توجه به تنوع سیستم های دنیای واقعی و خصوصیات بی شمار آنها، به طبع، ابزار فرمال متنوعی نیز برای بررسی آنها ابداع شده است. به عنوان نمونه بسیاری از ابزار مدلسازی فرمال قادر به نشان دادن دقیق خصوصیات سیستم های غیر موازی هستند. در مقابل بسیاری می توانند خصوصیات سیستم های موازی را که بسیار پیچیده ترند نشان دهند. همچنین خصوصیات ساختاری و رفتاری سیستم ها و نحوه برخورد آنها با زمان مسائل پیچیده ای است که باید در مدل سازی سیستم با ابزار فرمال مد نظر داشت.
با توجه به توضیحات ارائه شده در بخش های گذشته، می توان جدول مقایسه ای برای چهار ابزار توصیف فرمال مذکور به صورت جدول 2.1 ارائه داد.
جدول 2.1. خلاصه مقایسه ابزار توصیف فرمال
ردیف خصوصیت ابزار توصیف فرمال
ASM LOTOS VDM-SL Petri nets
1 پارادایم مبتنی بر جبر مبتنی بر جبر مبتنی بر مدل مبتنی بر مدل
2 سطح فرمالیتی فرمال فرمال فرمال فرمال
3 ابزار گرافیکی برای نمایش ندارد ندارد ندارد دارد
4 قابلیت توصیف سیستمهای موازی ندارد دارد ندارد دارد
5 قابلیت بیان[78] ضعیف ضعیف ضعیف قوی
6 قابلیت انتزاع پذیری متوسط متوسط متوسط قوی
7 پشتیبانی از شئی گرایی ندارد دارد ندارد دارد
8 قابلیت تبدیل به کد اجرایی دارد دارد دارد دارد
9 استفاده از متغیرها بله بله بله بله
10 قابلیت توصیف سیستم های غیر تعینی[79] ندارد دارد ندارد دارد
11 قابلیت اثبات پذیری دارد دارد دارد دارد
12 امکان بررسی مدل[80] ندارد ندارد دارد دارد
با توجه به نتایج به دست آمده از مقایسه ابزار مذکور و ماهیت سیستم مورد بررسی، در این تحقیق از زبان شبکه های پتری برای مدل سازی فرمال سیستم استفاده خواهد شد. به همین دلیل در این فصل در مورد این ابزار تمرکز و بررسی بیشتری به کار رفته است. همچنین در پایان کلیه قضایا و فرضیاتی که در طول تحقیق از آنها بهره گرفته می شود آمده است.
در فصل بعد به تشریح تکنولوژی مجازی سازی خواهیم پرداخت. این تکنولوژی برای ساخت لایه نرم افزاری دیتا سنتر به کار خواهد رفت. در نهایت در فصل چهار، مدل های فرمالی در چند لایه از دیتا سنتری که به کمک این تکنولوژی ساخته شده طراحی خواهیم کرد.
فصل سوم: بررسی معماری دیتا سنترها
در این بخش لازم است معماری زیر ساخت نرم افزاری دیتا سنترها را بررسی و تحلیل نمائیم. این تحلیل پیش نیاز ما در طراحی مدل فرمال این زیر ساخت خواهد بود. به این منظور، در ابتدا معماری نرم افزارهای مدیریت ماشین های مجازی تحت عنوان نرم افزارهای Hypervisor را بررسی و تشریح می نمائیم ]37[ و ]38[.
در حال حاضر سه نرم افزار مطرح در این زمینه، بیشترین سهم بازار سیستم های مجازی سازی را در اختیار دارند. این سه محصول عبارتند از:
Microsoft Hyper-V
Xen
VMware ESXi
از دیدگاه های مختلفی می توان hypervisor ها را با یکدیگر مقایسه نمود. از آن جمله می توان به پیاده سازی سرویس مجازی سازی کامل[81] در مقابل مجازی سازی ضمنی[82] اشاره کرد. در حالت اول، سخت افزار به طور کامل شبیه سازی می گردد و انتزاع کاملی از آن برای ماشین های مجازی ایجاد می گردد. به این ترتیب سیستم های عامل میهمان[83] نیازی به اصلاح برای کار بر روی این ماشین مجازی نخواهند داشت. همچنین آنها و نرم افزارهای در حال اجرا بر روی آنها هیچ اطلاعی از وجود ماشین مجازی نخواهند داشت. در نتیجه پیاده سازی به شکل کامل امکان مهاجرت نرم افزارها و سیستم های عامل میهمان بین ماشین های فیزیکی را میسر می سازد. همچنین با ایزوله کردن نرم افزارها و سیستم عامل ها، امنیت هر یک از آنها در حد بالایی تامین خواهد شد.
در عین حال این شکل از مجازی سازی مشکلات کاهش کارایی را نیز به دنبال دارد. زیرا hypervisor مجبور است تصویر کاملی از هر ماشین مجازی و سیستم عامل میهمان نصب شده بر روی آن را نگه دارد. به عنوان مثال حتی BIOS شبیه سازی می گردد. بنابراین منابع بیشتری صرف مدیریت و اجرای hypervisor خواهد شد.
در مقابل، پیازی سازی مجازی سازی به شکل ضمنی اجازه دسترسی سیستم های عامل میهمان را به بخش هایی از منابع بدون شبیه سازی آنها فراهم می کند. در این حالت لازم است روی سیستم های عامل میهمان اصلاحاتی صورت گیرد تا امکان برقراری ارتباط با hypervisor را داشته باشند. در نتیجه آنها از وجود ماشین مجازی مطلع خواهند بود. این روش در کنار برخی از مشکلات امنیتی، عموما از سیستم های عامل closed-source پشتیبانی نمی کند زیرا امکان انجام اصلاحات لازم برای کار در ماشین مجازی در مورد آنها وجود ندارد ]39[.
نرم افزارهای Hyper-V و Xen به صورت مجازی سازی ضمنی و ESX به صورت مجازی سازی مطلق پیاده سازی شده اند.
در ادامه به بررسی معماری هر یک از این سه محصول می پردازم و در نهایت برای مدل سازی روابط بر روی VMware ESX متمرکز خواهیم شد.
Microsoft Hyper-V
توضیحات زیر از سایت رسمی اسناد فنی شرکت میکروسافت (MSDN) برداشت شده است ]40[.
Hyper-V یک تکنولوژی مجازی سازی مبتنی بر Hypervisor است که برای Windows server 2008 نسخه 64 بیتی ساخته شده است.
اولین مفهوم مطرح در این تکنولوژی نوعی از جدا سازی[84] به نام پارتیشن است. در واقع Hyper-V از این بخش های جدا شده برای نگهداری اطلاعات و اجرای سیستم عامل های مختلف استفاده می کند. وجود حداقل یک پارتیشن ضروری است که پارتیشن ریشه یا والد[85] نامیده می شود. در این پارتیشن یک سیستم عامل Windows server 2008 نصب و اجرا می گردد که وظیفه مدیریت دیگر سیستم عامل های مهمان و برقراری ارتباط آنها با سخت افزارهای فیزیکی را بر عهده دارد. پارتیشن ریشه تنها پارتیشنی است که دسترسی مستقیم به سخت افزار فیزیکی را دارد و از طریق رابط برنامه نویسی[86] hypercall سیستم عامل های میهمان را ایجاد می کند.
سیستم عامل های میهمان با تصویری از پردازنده و وقفه ها[87] و در فضای محدودی از حافظه کار می کنند. در واقع hypervisor وقفه ها را برای سیستم عامل ترجمه کرده و به پارتیشن متناظر ارسال می کند. همچنین سیستم عامل ها (میهمان) به کمک ماژول VDev [88] با تصویری از سخت افزارهای جانبی کار می کنند که توسط hypervisor اجرا می شود. درخواست سیستم عامل از سخت افزار[89] مجازی توسط VMBus[90] که یک کانال ارتباطی منطقی بین پارتیشن ها است به hypervisor و یا پارتیشن ریشه منتقل می شود و از آنجا به سخت افزار واقعی انتقال می یابد. به عبارت دقیقتر، ماژول VSC[91] بر روی سیستم عامل میهمان درخواست خود را از طریق VMBus برای ماژول VSP[92] بر روی سیستم عامل میزبان در پارتیشن ریشه ارسال می نماید.
همچنین می توان از امکان Enlightened I/O برای افزایش سرعت و کارایی دستیابی به سخت افزارهای جانبی مانند دیسک، رابط شبکه و غیره استفاده نمود. در واقع این تکنولوژی، پیاده سازی پروتکل های سطح بالا (مانند SCSI) است که برای استفاده در محیط مجازی آماده پیاده سازی پروتکل های سطح بالا (مانند SCSI) است که برای استفاده در محیط مجازی آماده شده اند[93]. این پروتکل ها با استفاده مستقیم از VMBus، لایه های میانی شبیه سازی[94] سخت افزارها و نیاز به راه اندازها[95] را از بین می برند. اما استفاده از این امکان به راه اندازی سرویس های مجتمع سازی[96] نیاز دارد که برای چند سیستم عامل مشخص موجود است.
لیست سیستم های عاملی که توسط Hyper-V پشتیبانی می شوند در جدول 3.1 آورده شده است.
جدول 3.1. سیستم های عامل قابل پشتیبانی توسط Hyper-V R2 ]42[
Guest OS Virtual processors Edition(s)
Windows 71,2 or 4 Both x86-32 and x86-64, all editions except home editions
Windows Server 2008 R21,2 or 4 Web, Standard, Enterprise, Datacenter
Windows Server 20081,2 or 4 Both x86 and x64, Web, HPC, Standard, Enterprise, Datacenter, with or without Hyper-V
Linux (only including SUSE Linux Enterprise Server 10 with SP3 or version 11 and Red Hat Linux versions 5.2-5.5) 1,2 or 4 Both x86 and x64
Windows Server 20031 or 2 Both x86 and x64, Standard, Enterprise, Datacenter, SP2 required
Windows Server 2003 R21 or 2 Web, Standard, Enterprise, Datacenter, both x86 and x64 except for Web whose 64-bit version is not supported
Windows Vista1 or 2 Both x86 and x64, all editions except home editionsOthers 1 N/A
شمایی از معماری Hyper-V در شکل 3.1 آورده شده است.
شکل 3.1. معماری سطح بالای Hyper-V ]40[
بررسی اجزاء معماری Hyper-V
در ادامه به توضیح مختصری درباره بخش ها و اصطلاحات این معماری می پردازیم.
APIC[97]
ماژولی که امکان اولویت بندی وقفه ها را فراهم می سازد.
Child Partition
پارتیشنی که حاوی یک سیستم عامل میهمان است. تمام دسترسی های لازم به منابع فیزیکی سیستم مانند حافظه و وسایل جانبی توسط VMBus و hypervisor برای این پارتیشن فراهم می گردد.
Hypercall
رابطی برای ارتباط با hypervisor است که از طریق آن سیستم های عامل میهمان می توانند به ابزار بهینه hypervisot دست یابند.
Hypervisor
یک لایه نرم افزاری که مابین سخت افزار و یک یا چند سیستم عامل قرار می گیرد و وظیفه اصلی آن فراهم آوردن فضای مجزایی به نام پارتیشن برای اجرای هر یک از سیستم های عامل است. Hypervisor دسترسی به سخت افزار را کنترل و مدیریت می کند.
IC[98]
ماژولی است که امکان ارتباط سیستم های عامل میهمان را با یکدیگر و با hypervisor فراهم می آورد.
I/O stack
همان پشته ورودی و خروجی است.
Root Partition
پارتیشنی است که سیستم عامل آن وظایف مدیریتی در سطح ماشین را انجام می دهد که عبارتند از راه انداز سخت افزارهای جانبی، مدیریت انرژی مصرفی و اضافه و حذف کردن دستگاه های در حال کار. این پارتیشن تنها پارتیشنی است که دسترسی مستقیمی منابع فیزیکی سیستم دارد.
VID[99]
عملیاتی مانند سرویس های مدیریت پارتیشن ها، سرویس مدیریت پردازنده های مجازی، و سرویس مدیریت حافظه برای پارتیشن ها را ارائه می دهد.
VMBus
یک مکانیزم ارتباطی مبتنی بر کانال برای ارتباط پارتیشن ها و دستگاه ها فراهم می آورد.
VMMS[100]
مدیریت وضعیت همه ماشین های مجازی در پارتیشن های فرزند را بر عهده دارد.
VMWP[101]
یک بخش user mode در پشته مجازی سازی است. با این تعریف که پروسه ایجاد کننده[102] یک سرویس مدیریت ماشین ها مجازی در پارتیشن ریشه (windows server 2008) ایجاد می کند که به کمک آن می توان سیستم های عامل میهمان را مدیریت نمود، سرویس VMWP یک پروسه ایجاد کننده مجزا برای هر یک از پارتیشن های فرزند ایجاد می کند.
VSC[103]
یک ماژول ترکیبی که که در پارتیشن فرزند قرار می گیرد و نحوه استفاده از منابع سخت افزاری را که توسط سرویس دهنده مجازی (VSP) ارائه شده بهینه می نماید. VSC با VSP متناظر خود در پارتیشن ریشه از طریق VMBus ارتباط برقرار می کند تا به درخواست های I/O پارتیشن فرزند سرویس دهد.
VSP[104]
سرویسی که در پارتیشن ریشه قرار می گیرد و از درخواست های پارتیشن های فرزند که از طریق VMBus مطرح می شود پاسخ می دهد.
WinHv[105]
این ماژول پلی بین راه اندازهای سیستمهای عامل موجود در پارتیشن ها و hypervisor است که به راه اندازها امکان می هد تا از طریق رابط فراخوانی استاندارد ویندوز، hypervisor را صدا بزنند.
WMI[106]
ابزار مدیریت ویندوز مجموعه ای از API ها هستند که سرویس مدیریت ماشین های مجازی برای مدیریت و کنترل ماشین ها ارائه می دهد.
نقاط ضعف
در مجموع می توان گفت که Hyper-V زیر ساخت نسبتا سبکی برای پیاده سازی ساختار مجازی سازی است. در عین حال به دلیل نیاز به وجود بخشی از معمای در سیستم های عامل میهمان، اجرای آنها کاملا مستقل از hypervisor نخواهد بود. در عمل نیز می بینیم که Hyper-V از تعداد محدودی از سیستم های عامل به عنوان میهمان پشتیبانی می کند تعدادی از آنها در جدول 3.1 آمده است.
همچنین نیاز به وجود یک سیستم عامل میزبان[107] هنوز هم وجود دارد. به این معنی که یک Windows server 2008 باید در پارتیشن ریشه نصب گردد تا بتواند درخواست های سیستم های عامل میهمان از سخت افزارهای مجازی را به سخت افزارهای فیزیکی منتقل نماید ]43[.
برای مطالعه بیشتر در مورد Microsoft Hyper-V به ]44[ الی ]48[ مراجعه کنید.
Xen
در این بخش به تشریح کلیات معماری نرم افزار مجازی سازی Xen خواهیم پرداخت ]49[ و ]50[. این hypervisor معروفترین نرم افزار مجازی سازی با متن باز است که شرکت ها و سازمان های متعددی با بومی سازی از آن برای پیاده سازی زیر ساخت مجازی خود استفاده کرده اند. Xen به صورت یک مجازی ساز ضمنی پیاده سازی شده است بنابراین برای سیستم های عامل میهمان برای کار با آن نیاز به یک سری تغییراتی دارند.
لیست سیستم های عاملی که توسط Xen 3.0 پشتیبانی می شوند در جدول 3.2 آورده شده است.
جدول 3.2. سیستم های عامل قابل پشتیبانی توسط Xen نسخه 3
Operating Sys– Runs as Dom0 (host os) Runs as DomU (guest os)
Linux 2.6 Yes Yes
NetBSD 3.1 No Yes
NetBSD 4.0_BETA2 and -CURRENT Yes Yes
FreeBSD 5.3 No currently broken? Actively being worked on
FreeBSD 7-CURRENT no can be patched; works.
Plan 9 No currently broken?
ReactOS No planned, development stalled