Verve (operating system)
વર્વ એ માઈક્રોસોફ્ટ રિસર્ચ દ્વારા વિકસાવવામાં આવેલી એક રિસર્ચ ઓપરેટિંગ સિસ્ટમ છે. પ્રકાર સલામતી અને મેમરી સલામતી માટે વર્વની એન્ડ-ટુ-એન્ડ ચકાસણી કરવામાં આવે છે. તેમની જટિલતાને કારણે, ઓપરેટિંગ સિસ્ટમ્સના ગુણધર્મોને ચકાસવા માટે સોફ્ટવેર ચકાસણીની પવિત્ર તક આપવામાં આવી છે. ઓપરેટિંગ સિસ્ટમ્સ સામાન્ય રીતે નિમ્ન-સ્તરની ભાષાઓમાં લખવામાં આવે છે, જેમ કે સી, જે ખૂબ ઓછી બાંયધરી આપે છે. સિંગ્યુલારિટી પ્રોજેક્ટે સી #માં ઓપરેટિંગ સિસ્ટમ લખવાનો અભિગમ અપનાવ્યો, જે એક પ્રકાર-સલામત, મેમરી-સલામત ભાષા છે. આ અભિગમની નબળાઈ એ છે કે ઓપરેટિંગ સિસ્ટમોએ જરૂરી રીતે નીચલા-સ્તરના કોડને કૉલ કરવાની જરૂર છે, ઉદાહરણ તરીકે, સ્ટેક પોઇન્ટરને ખસેડો. વર્વ ઓપરેટિંગ સિસ્ટમને ચકાસાયેલ એસેમ્બલી ભાષામાં વિભાજીત કરીને આ સમસ્યાનું સમાધાન કરે છે જે સી #માં લખાયેલ બાકીની ઓપરેટિંગ સિસ્ટમ માટે નિમ્ન-સ્તર અને વિશ્વસનીય ઇન્ટરફેસ હોવું જરૂરી છે. એક વિશ્વસનીય સ્પષ્ટીકરણ છે જે બાંહેધરી આપે છે કે નિમ્ન-સ્તરનો એસેમ્બલી કોડ ઢગલામાં ફેરફાર કરતું નથી અને ઉચ્ચ-સ્તરનો સી #કોડ સ્ટેક્સમાં ફેરફાર કરતું નથી. વર્વમાં એક નાનું ન્યુક્લિયસ હોય છે, જે ન્યૂનતમ હાર્ડવેર એબ્સ્ટ્રેક્શન સ્તર તરીકે કામ કરે છે, અને એક કર્નલ હોય છે, જે ન્યુક્લિયસ દ્વારા પૂરા પાડવામાં આવેલ પ્રિમિટિવ્સનો ઉપયોગ કરે છે જેથી એપ્લિકેશનો માટે વધુ પરંપરાગત ઇન્ટરફેસને ખુલ્લી પાડી શકાય. ન્યુક્લિયસ સિવાય સિસ્ટમના તમામ ઘટકો સંચાલિત કોડ સી #માં લખવામાં આવે છે અને બાર્ટોક (મૂળરૂપે સિંગ્યુલારિટી પ્રોજેક્ટ માટે વિકસાવવામાં આવેલ) દ્વારા ટાઇપ કરેલ એસેમ્બલી લેંગ્વેજ (ટી. એ. એલ.) માં સંકલિત કરવામાં આવે છે, જે ટી. એ. એલ. ચેકર દ્વારા ચકાસવામાં આવે છે. ન્યુક્લિયસ મેમરી એલોકેટર અને કચરો સંગ્રહ, સ્ટેક સ્વિચિંગ માટે સપોર્ટ અને ઇન્ટરપ્ટ હેન્ડલર્સનું સંચાલન કરે છે. તે બૂગીપીએલમાં લખાયેલું છે, જે એમએસઆરના બૂગી ચકાસણીકર્તાના ઇનપુટ તરીકે કામ કરે છે, જે ઝેડ3 પ્રમેય પ્રોવર સંતોષકારક મોડ્યુલો સિદ્ધાંતો (એસએમટી) સ્વચાલિત પ્રમેય પ્રોવર (સોલ્વર) નો ઉપયોગ કરીને ન્યુક્લિયસને સાચું સાબિત કરે છે. ન્યુક્લિયસ થ્રેડો, સમયપત્રક, સુમેળને અમલમાં મૂકવા અને મોટાભાગના વિક્ષેપ હેન્ડલર્સ પ્રદાન કરવા માટે કર્નલ પર આધાર રાખે છે. ભલે કર્નલ ઔપચારિક રીતે ચકાસાયેલ ન હોય, તેથી, ઉદાહરણ તરીકે, સમયપત્રકમાં ખામી સિસ્ટમને લટકાવી શકે છે, તે પ્રકાર અથવા મેમરી સલામતીનું ઉલ્લંઘન કરી શકતી નથી, અને આમ સીધી રીતે અવ્યાખ્યાયિત વર્તનનું કારણ બની શકતી નથી. જો તે ન્યુક્લિયસને અમાન્ય વિનંતીઓ કરવાનો પ્રયાસ કરે છે, તો ઔપચારિક ચકાસણી ખાતરી આપે છે કે ન્યુક્લિયસ પરિસ્થિતિને નિયંત્રિત રીતે સંભાળે છે. વર્વનો વિશ્વસનીય કમ્પ્યુટિંગ આધાર (ટી. સી. બી.) આ સુધી મર્યાદિત છેઃ ન્યુક્લિયસની ચોકસાઈની ચકાસણી કરવા માટે બૂગી/ઝેડ3; તેને x86 એસેમ્બલીમાં અનુવાદિત કરવા માટે બૂગીએએસએમ; ન્યુક્લિયસે કેવી રીતે વર્તવું જોઈએ તેનું બૂગીઈપીએલ સ્પષ્ટીકરણ; ટીએએલ ચકાસણી કરનાર; એસેમ્બલર અને લિંકર; અને બૂટલોડર. નોંધપાત્ર રીતે, ન તો સી #કમ્પાઇલર/રનટાઇમ કે ન તો બાર્ટોક કમ્પાઇલર ટીસીબીનો ભાગ છે. છેલ્લી સૂચના માટે સલામત સંદર્ભોઃ ટાઇપ-સેફ ઓપરેટિંગ સિસ્ટમની સ્વચાલિત ચકાસણી, જીન યાંગ અને ક્રિસ હોબ્લિટ્ઝેલ. પ્રોગ્રામિંગ લેંગ્વેજ ડિઝાઇન અને અમલીકરણ, 2010. સેફ ટુ ધ લાસ્ટ ઇન્સ્ટ્રક્શનઃ ટાઇપ-સેફ ઓપરેટિંગ સિસ્ટમની ઓટોમેટેડ વેરિફિકેશન, જીન યાંગ અને ક્રિસ હોબ્લિટ્ઝેલ. સી. એ. સી. એમ. સંશોધન હાઇલાઇટ. એસીએમના સંદેશાવ્યવહાર, સપ્ટેમ્બર 2010. ટેકનિકલ પરિપ્રેક્ષ્યઃ સલામતી પ્રથમ! વર્વઃ એક પ્રકારની સલામત ઓપરેટિંગ સિસ્ટમ. ક્રિસ હોબ્લિટ્ઝેલ સાથેની મુલાકાત. વર્વઃ એક પ્રકારની સલામત ઓપરેટિંગ સિસ્ટમ. ઓ. એસ. ન્યૂઝ. વર્વની જાહેરાત-એક પ્રકાર-સલામત ઓપરેટિંગ સિસ્ટમ. માહિતી. માઈક્રોસોફ્ટ ઓપરેટિંગ સિસ્ટમ્સ માઈક્રોસોફ્ટ રિસર્ચ માઇક્રોકર્નલ-આધારિત ઓપરેટિંગ સિસ્ટમ્સ માઇક્રોકર્નલ નેનોકર્નલ